>imtrd

Theorem.

Arguments:

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

Hypotheses:

(phito(chileftrightarrowtau))
(phito(psileftrightarrowtheta))
(phito(psitochi))

Assertions:

(phito(thetatotau))

Proof:

Hyp Ref Line Expr
Hypo1(phito(chileftrightarrowtau))
2(phito(psileftrightarrowtheta))
3(phito(psitochi))
2bi<4(phito(thetatopsi))
3, 4syld5(phito(thetatochi))
1bi>6(phito(chitotau))
5, 6syld7(phito(thetatotau))