rp-2<

Theorem.

Arguments:

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

Hypotheses:

(ceqb)
(phito(aeqb))

Assertions:

(phito(aeqc))

Proof:

Hyp Ref Line Expr
Hypo1(ceqb)
2(phito(aeqb))
1ax-sym3(beqc)
2, 3rp-2>4(phito(aeqc))