sb-an

Theorem.

Arguments:

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

Assertions:

([a/x](phiwedgepsi)leftrightarrow([a/x]phiwedge[a/x]psi))

Proof:

Hyp Ref Line Expr
an.or1((phiwedgepsi)leftrightarrowlnot(lnotphiveelnotpsi))
1bi.bldsb2([a/x](phiwedgepsi)leftrightarrow[a/x]lnot(lnotphiveelnotpsi))
sb-neg3([a/x]lnot(lnotphiveelnotpsi)leftrightarrowlnot[a/x](lnotphiveelnotpsi))
sb-or4([a/x](lnotphiveelnotpsi)leftrightarrow([a/x]lnotphivee[a/x]lnotpsi))
sb-neg5([a/x]lnotphileftrightarrowlnot[a/x]phi)
sb-neg6([a/x]lnotpsileftrightarrowlnot[a/x]psi)
5, 6bi.bldor<>7(([a/x]lnotphivee[a/x]lnotpsi)leftrightarrow(lnot[a/x]phiveelnot[a/x]psi))
4, 7bitr8([a/x](lnotphiveelnotpsi)leftrightarrow(lnot[a/x]phiveelnot[a/x]psi))
8bi.bldneg9(lnot[a/x](lnotphiveelnotpsi)leftrightarrowlnot(lnot[a/x]phiveelnot[a/x]psi))
2, 3, 92bitr10([a/x](phiwedgepsi)leftrightarrowlnot(lnot[a/x]phiveelnot[a/x]psi))
an.or11(([a/x]phiwedge[a/x]psi)leftrightarrowlnot(lnot[a/x]phiveelnot[a/x]psi))
10, 11><bitr12([a/x](phiwedgepsi)leftrightarrow([a/x]phiwedge[a/x]psi))