eu.or

Theorem.

Arguments:

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

Hypotheses:

(x bound in phi)

Assertions:

((lnotphiwedge_e1xpsi)to_e1x(phiveepsi))

Proof:

Hyp Ref Line Expr
Hypo1(x bound in phi)
1bv-¬2(x bound in lnotphi)
or-false3(lnotphito(psileftrightarrow(phiveepsi)))
2, 3eqt-∃1-d4(lnotphito(_e1xpsileftrightarrow_e1x(phiveepsi)))
4bi>an5((lnotphiwedge_e1xpsi)to_e1x(phiveepsi))