sb-xplw

Theorem.

Arguments:

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

Distinct variable conditions:

(a, x),

Hypotheses:

((xeqa)to(phileftrightarrowpsi))
(x bound in psi)

Assertions:

([a/x]phileftrightarrowpsi)

Proof:

Hyp Ref Line Expr
Hypo1((xeqa)to(phileftrightarrowpsi))
2(x bound in psi)
2sb-bv3([a/x]psileftrightarrowpsi)
sb-eqat<xw4[a/x](xeqa)
1, 4im.bldsb5[a/x](phileftrightarrowpsi)
3, 5sb-bi>6([a/x]phileftrightarrowpsi)