sylan>

Theorem.

Arguments:

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

Hypotheses:

(thetatopsi)
((phiwedgepsi)tochi)

Assertions:

((phiwedgetheta)tochi)

Proof:

Hyp Ref Line Expr
Hypo1(thetatopsi)
2((phiwedgepsi)tochi)
2exp3(phito(psitochi))
1, 3rpi324(phito(thetatochi))
4imp5((phiwedgetheta)tochi)