bi.bldsbt

Theorem.

Arguments:

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

Assertions:

(forallx(phileftrightarrowpsi)to([y/x]phileftrightarrow[y/x]psi))

Proof:

Hyp Ref Line Expr
spec1(forallx(phileftrightarrowpsi)to[y/x](phileftrightarrowpsi))
sb-bi2([y/x](phileftrightarrowpsi)leftrightarrow([y/x]phileftrightarrow[y/x]psi))
1, 2brpi223(forallx(phileftrightarrowpsi)to([y/x]phileftrightarrow[y/x]psi))