<bsylan>

Theorem.

Arguments:

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

Hypotheses:

(psileftrightarrowtheta)
((phiwedgepsi)tochi)

Assertions:

((phiwedgetheta)tochi)

Proof:

Hyp Ref Line Expr
Hypo1(psileftrightarrowtheta)
2((phiwedgepsi)tochi)
1bi<3(thetatopsi)
2, 3sylan>4((phiwedgetheta)tochi)