>bid

Theorem.

Arguments:

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

Hypotheses:

(phito(chitopsi))
(phito(psitochi))

Assertions:

(phito(psileftrightarrowchi))

Proof:

Hyp Ref Line Expr
Hypo1(phito(chitopsi))
2(phito(psitochi))
1, 2jca3(phito((psitochi)wedge(chitopsi)))
dfbi4((psileftrightarrowchi)leftrightarrow((psitochi)wedge(chitopsi)))
3, 4brpi22<5(phito(psileftrightarrowchi))