bi.bldnegd

Theorem.

Arguments:

phi (pr), psi (pr), chi (pr),

Hypotheses:

(phito(psileftrightarrowchi))

Assertions:

(phito(lnotpsileftrightarrowlnotchi))

Proof:

Hyp Ref Line Expr
Hypo1(phito(psileftrightarrowchi))
conb2((psileftrightarrowchi)leftrightarrow(lnotpsileftrightarrowlnotchi))
1, 2brpi223(phito(lnotpsileftrightarrowlnotchi))