eqt<>

Theorem.

Arguments:

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

Assertions:

(((aeqb)wedge(ceqd))to((alec)leftrightarrow(bled)))

Proof:

Hyp Ref Line Expr
eqt<1((aeqb)to((alec)leftrightarrow(blec)))
eqt>2((ceqd)to((blec)leftrightarrow(bled)))
1, 2bsylan93(((aeqb)wedge(ceqd))to((alec)leftrightarrow(bled)))