eqt<>

Theorem.

Arguments:

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

Assertions:

(((aeqb)wedge(ceqd))to((aeqc)leftrightarrow(beqd)))

Proof:

Hyp Ref Line Expr
eqt<1((aeqb)to((aeqc)leftrightarrow(beqc)))
eqt>2((ceqd)to((beqc)leftrightarrow(beqd)))
1siman<3(((aeqb)wedge(ceqd))to((aeqc)leftrightarrow(beqc)))
2siman>4(((aeqb)wedge(ceqd))to((beqc)leftrightarrow(beqd)))
3, 4bitrd5(((aeqb)wedge(ceqd))to((aeqc)leftrightarrow(beqd)))