<2trg

Theorem.

Arguments:

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

Hypotheses:

(deqb)
(ceqa)
(phito(aleb))

Assertions:

(phito(cled))

Proof:

Hyp Ref Line Expr
Hypo1(deqb)
2(ceqa)
3(phito(aleb))
2eqsym4(aeqc)
1eqsym5(beqd)
3, 4, 5>2trg6(phito(cled))