eq-sb>b

Theorem.

Arguments:

a (st), x (sv), phi (pr),

Assertions:

((xeqa)to(phileftrightarrow[a/x]phi))

Proof:

Hyp Ref Line Expr
eqt-sb1((xeqa)to([x/x]phileftrightarrow[a/x]phi))
sbid2([x/x]phileftrightarrowphi)
2ax13((xeqa)to([x/x]phileftrightarrowphi))
1, 3<>bitrd4((xeqa)to(phileftrightarrow[a/x]phi))