sb-im

Theorem.

Arguments:

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

Assertions:

([a/x](phitopsi)leftrightarrow([a/x]phito[a/x]psi))

Proof:

Hyp Ref Line Expr
im.or1((phitopsi)leftrightarrow(lnotphiveepsi))
1bi.bldsb2([a/x](phitopsi)leftrightarrow[a/x](lnotphiveepsi))
sb-or3([a/x](lnotphiveepsi)leftrightarrow([a/x]lnotphivee[a/x]psi))
sb-neg4([a/x]lnotphileftrightarrowlnot[a/x]phi)
4bi.bldor<5(([a/x]lnotphivee[a/x]psi)leftrightarrow(lnot[a/x]phivee[a/x]psi))
2, 3, 52bitr6([a/x](phitopsi)leftrightarrow(lnot[a/x]phivee[a/x]psi))
im.or7(([a/x]phito[a/x]psi)leftrightarrow(lnot[a/x]phivee[a/x]psi))
6, 7><bitr8([a/x](phitopsi)leftrightarrow([a/x]phito[a/x]psi))