sb-bi

Theorem.

Arguments:

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

Assertions:

([a/x](phileftrightarrowpsi)leftrightarrow([a/x]phileftrightarrow[a/x]psi))

Proof:

Hyp Ref Line Expr
dfbi1((phileftrightarrowpsi)leftrightarrow((phitopsi)wedge(psitophi)))
1bi.bldsb2([a/x](phileftrightarrowpsi)leftrightarrow[a/x]((phitopsi)wedge(psitophi)))
sb-an3([a/x]((phitopsi)wedge(psitophi))leftrightarrow([a/x](phitopsi)wedge[a/x](psitophi)))
sb-im4([a/x](phitopsi)leftrightarrow([a/x]phito[a/x]psi))
sb-im5([a/x](psitophi)leftrightarrow([a/x]psito[a/x]phi))
4, 5bi.bldan<>6(([a/x](phitopsi)wedge[a/x](psitophi))leftrightarrow(([a/x]phito[a/x]psi)wedge([a/x]psito[a/x]phi)))
2, 3, 62bitr7([a/x](phileftrightarrowpsi)leftrightarrow(([a/x]phito[a/x]psi)wedge([a/x]psito[a/x]phi)))
dfbi8(([a/x]phileftrightarrow[a/x]psi)leftrightarrow(([a/x]phito[a/x]psi)wedge([a/x]psito[a/x]phi)))
7, 8><bitr9([a/x](phileftrightarrowpsi)leftrightarrow([a/x]phileftrightarrow[a/x]psi))