2bitrd

Theorem.

Arguments:

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

Hypotheses:

(phito(thetaleftrightarrowtau))
(phito(chileftrightarrowtheta))
(phito(psileftrightarrowchi))

Assertions:

(phito(psileftrightarrowtau))

Proof:

Hyp Ref Line Expr
Hypo1(phito(thetaleftrightarrowtau))
2(phito(chileftrightarrowtheta))
3(phito(psileftrightarrowchi))
2, 3bitrd4(phito(psileftrightarrowtheta))
1, 4bitrd5(phito(psileftrightarrowtau))