<bsylan<

Theorem.

Arguments:

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

Hypotheses:

(phileftrightarrowtheta)
((phiwedgepsi)tochi)

Assertions:

((thetawedgepsi)tochi)

Proof:

Hyp Ref Line Expr
Hypo1(phileftrightarrowtheta)
2((phiwedgepsi)tochi)
1bi<3(thetatophi)
2, 3sylan<4((thetawedgepsi)tochi)