Theorem oridm 901

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 900	. 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑)
2		pm2.07 899	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑))
3	1, 2	impbii 211	1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 208   ∨ wo 843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-or 844

This theorem is referenced by:  pm4.25  902  orordi  925  orordir  926  nornot  1523  truortru  1573  falorfal  1576  unidm  4121  dfsn2ALT  4580  preqsnd  4782  suceloni  7521  tz7.48lem  8070  msq0i  11280  msq0d  11282  prmdvdsexp  16054  metn0  22965  rrxcph  23990  nb3grprlem2  27161  pdivsq  33002  pm11.7  40802  euoreqb  43382