eqt<>i

Theorem.

Arguments:

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

Hypotheses:

(ceqd)
(aeqb)

Assertions:

((aeqc)leftrightarrow(beqd))

Proof:

Hyp Ref Line Expr
Hypo1(ceqd)
2(aeqb)
1, 2>andi3((aeqb)wedge(ceqd))
3eqt<>4((aeqc)leftrightarrow(beqd))