>2bitrd

Theorem.

Arguments:

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

Hypotheses:

(phito(chileftrightarrowtau))
(phito(psileftrightarrowtheta))
(phito(psileftrightarrowchi))

Assertions:

(phito(thetaleftrightarrowtau))

Proof:

Hyp Ref Line Expr
Hypo1(phito(chileftrightarrowtau))
2(phito(psileftrightarrowtheta))
3(phito(psileftrightarrowchi))
2bicom4(phito(thetaleftrightarrowpsi))
1, 3, 42bitrd5(phito(thetaleftrightarrowtau))