Theorem oridm 918

Description: 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.)

Assertion

Ref	Expression
oridm	⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)

Proof of Theorem oridm

Step	Hyp	Ref	Expression
1		pm1.2 917	. 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑)
2		pm2.07 916	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑))
3	1, 2	impbii 212	1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm4.25  919  orordi  942  orordir  943  nornot  1561  truortru  1607  falorfal  1610  unidm  4104  dfsn2ALT  4606  preqsnd  4819  tz7.48lemOLD  8451  msq0i  11965  msq0d  11966  prmdvdsexp  16891  metn0  24679  rrxcph  25713  nb3grprlem2  29962  pm11.7  45380  euoreqb  48179