Theorem oridm 902

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

Syntax hints:   ↔ wb 205   ∨ wo 844

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 206  df-or 845

This theorem is referenced by:  pm4.25  903  orordi  926  orordir  927  nornot  1529  truortru  1579  falorfal  1582  unidm  4091  dfsn2ALT  4587  preqsnd  4795  sucexeloni  7652  suceloniOLD  7654  tz7.48lem  8263  msq0i  11622  msq0d  11624  prmdvdsexp  16418  prmdvdssqOLD  16422  metn0  23511  rrxcph  24554  nb3grprlem2  27746  pm11.7  41984  euoreqb  44569