>2bitrg

Theorem.

Arguments:

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

Hypotheses:

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

Assertions:

(phito(thetaleftrightarrowtau))

Proof:

Hyp Ref Line Expr
Hypo1(chileftrightarrowtau)
2(psileftrightarrowtheta)
3(phito(psileftrightarrowchi))
2ax14(phito(psileftrightarrowtheta))
1ax15(phito(chileftrightarrowtau))
3, 4, 5>2bitrd6(phito(thetaleftrightarrowtau))