<>bitr

Theorem.

Arguments:

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

Hypotheses:

(psileftrightarrowchi)
(psileftrightarrowphi)

Assertions:

(phileftrightarrowchi)

Proof:

Hyp Ref Line Expr
Hypo1(psileftrightarrowchi)
2(psileftrightarrowphi)
2bicomi3(phileftrightarrowpsi)
1, 3bitr4(phileftrightarrowchi)