<>bitrd

Theorem.

Arguments:

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

Hypotheses:

(phito(chileftrightarrowtheta))
(phito(chileftrightarrowpsi))

Assertions:

(phito(psileftrightarrowtheta))

Proof:

Hyp Ref Line Expr
Hypo1(phito(chileftrightarrowtheta))
2(phito(chileftrightarrowpsi))
2bicom3(phito(psileftrightarrowchi))
1, 3bitrd4(phito(psileftrightarrowtheta))