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  1524  truortru  1574  falorfal  1577  unidm  4130  dfsn2ALT  4589  preqsnd  4791  suceloni  7530  tz7.48lem  8079  msq0i  11289  msq0d  11291  prmdvdsexp  16061  metn0  22972  rrxcph  23997  nb3grprlem2  27165  pdivsq  32983  pm11.7  40735  euoreqb  43315