trd-2r

Theorem.

Arguments:

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

Hypotheses:

(psito(beqc))
(phito(aeqb))

Assertions:

((psiwedgephi)to(aeqc))

Proof:

Hyp Ref Line Expr
Hypo1(psito(beqc))
2(phito(aeqb))
1, 2trd-23((phiwedgepsi)to(aeqc))
3ancom4((psiwedgephi)to(aeqc))