Theorem oridm

Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.) (Proof shortened by Andrew Salmon, 16-Apr-2011.) (Proof shortened by Wolf Lammen, 10-Mar-2013.)

Conclusion
\( \vdash \varphi \vee \varphi \leftrightarrow \varphi \)
Proof
l0
pm1.2
pm2.07
impbii l0 _