Theorem oibabs

Absorption of disjunction into equivalence. (Contributed by NM, 6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.)

Conclusion
\( \vdash \varphi \vee \psi \rightarrow (\varphi \leftrightarrow \psi) \leftrightarrow (\varphi \leftrightarrow \psi) \)
Proof
l0
norbi
id
l2
ja l0 _
ax-1
impbii l2 _