Theorem oridm 903

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 902	. 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑)
2		pm2.07 901	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑))
3	1, 2	impbii 209	1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 206   ∨ wo 846

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 207  df-or 847

This theorem is referenced by:  pm4.25  904  orordi  927  orordir  928  nornot  1528  truortru  1574  falorfal  1577  unidm  4180  dfsn2ALT  4669  preqsnd  4883  sucexeloniOLD  7846  suceloniOLD  7848  tz7.48lem  8497  msq0i  11937  msq0d  11939  prmdvdsexp  16762  metn0  24391  rrxcph  25445  nb3grprlem2  29416  pm11.7  44365  euoreqb  47024