<bsylan<>

Theorem.

Arguments:

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

Hypotheses:

(psileftrightarrowtau)
(phileftrightarrowtheta)
((phiwedgepsi)tochi)

Assertions:

((thetawedgetau)tochi)

Proof:

Hyp Ref Line Expr
Hypo1(psileftrightarrowtau)
2(phileftrightarrowtheta)
3((phiwedgepsi)tochi)
2, 3<bsylan<4((thetawedgepsi)tochi)
1, 4<bsylan>5((thetawedgetau)tochi)