<imtrd

Theorem.

Arguments:

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

Hypotheses:

(phito(tauleftrightarrowchi))
(phito(thetaleftrightarrowpsi))
(phito(psitochi))

Assertions:

(phito(thetatotau))

Proof:

Hyp Ref Line Expr
Hypo1(phito(tauleftrightarrowchi))
2(phito(thetaleftrightarrowpsi))
3(phito(psitochi))
2bicom4(phito(psileftrightarrowtheta))
1bicom5(phito(chileftrightarrowtau))
3, 4, 5>imtrd6(phito(thetatotau))