rp-2>

Theorem.

Arguments:

a (st), b (coll), c (coll),

Hypotheses:

(bequivc)
(ainb)

Assertions:

(ainc)

Proof:

Hyp Ref Line Expr
Hypo1(bequivc)
2(ainb)
1eqt>3((ainb)to(ainc))
2, 3ax-mp4(ainc)