Theorem oridm 915

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

Syntax hints:   ↔ wb 208   ∨ wo 858

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 859

This theorem is referenced by:  pm4.25  916  orordi  939  orordir  940  nornot  1551  truortru  1597  falorfal  1600  unidm  4110  dfsn2ALT  4604  preqsnd  4817  tz7.48lem  8412  msq0i  11836  msq0d  11837  prmdvdsexp  16750  metn0  24420  rrxcph  25454  nb3grprlem2  29582  pm11.7  44972  euoreqb  47703