eqi

Theorem.

Arguments:

a (obj), b (obj),

Hypotheses:

(blea)
(aleb)

Assertions:

(aeqb)

Proof:

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