rp-2>r

Theorem.

Arguments:

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

Hypotheses:

(beqc)
(phito(aeqb))

Assertions:

(phito(ceqa))

Proof:

Hyp Ref Line Expr
Hypo1(beqc)
2(phito(aeqb))
1, 2rp-2>3(phito(aeqc))
3ax-sym4(phito(ceqa))