>2trg

Theorem.

Arguments:

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

Hypotheses:

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

Assertions:

(phito(ceqd))

Proof:

Hyp Ref Line Expr
Hypo1(beqd)
2(aeqc)
3(phito(aeqb))
2, 3rp-1>4(phito(ceqb))
1, 4rp-2>5(phito(ceqd))