trd-2r

Theorem.

Arguments:

a (obj), b (obj), c (obj), phi (pr), psi (pr),

Hypotheses:

(psito(blec))
(phito(aleb))

Assertions:

((psiwedgephi)to(alec))

Proof:

Hyp Ref Line Expr
Hypo1(psito(blec))
2(phito(aleb))
2siman>3((psiwedgephi)to(aleb))
1siman<4((psiwedgephi)to(blec))
3, 4trd5((psiwedgephi)to(alec))