Theorem oridm 910

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 909	. 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑)
2		pm2.07 908	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑))
3	1, 2	impbii 210	1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 207   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  pm4.25  911  orordi  934  orordir  935  nornot  1538  truortru  1584  falorfal  1587  unidm  4087  dfsn2ALT  4577  preqsnd  4790  tz7.48lem  8370  msq0i  11790  msq0d  11791  prmdvdsexp  16676  metn0  24343  rrxcph  25377  nb3grprlem2  29468  pm11.7  44840  euoreqb  47572