trd

Theorem.

Arguments:

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

Hypotheses:

(phito(blec))
(phito(aleb))

Assertions:

(phito(alec))

Proof:

Hyp Ref Line Expr
Hypo1(phito(blec))
2(phito(aleb))
2ax-tr3(phito((blec)to(alec)))
1, 3mpd4(phito(alec))