trd>

Theorem.

Arguments:

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

Hypotheses:

(phito(aeqc))
(phito(aeqb))

Assertions:

(phito(beqc))

Proof:

Hyp Ref Line Expr
Hypo1(phito(aeqc))
2(phito(aeqb))
2ax-sym3(phito(beqa))
1, 3trd4(phito(beqc))