rp-1>g

Theorem.

Arguments:

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

Hypotheses:

(aeqc)
(phito(aleb))

Assertions:

(phito(cleb))

Proof:

Hyp Ref Line Expr
Hypo1(aeqc)
2(phito(aleb))
1eqsym3(ceqa)
2, 3rp-1<g4(phito(cleb))