eqd

Theorem.

Arguments:

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

Hypotheses:

(phito(blea))
(phito(aleb))

Assertions:

(phito(aeqb))

Proof:

Hyp Ref Line Expr
Hypo1(phito(blea))
2(phito(aleb))
1, 2jca3(phito((aleb)wedge(blea)))
3df-equ4(phito(aeqb))