Theorem oridm 929

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 928	. 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑)
2		pm2.07 927	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑))
3	1, 2	impbii 201	1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 198   ∨ wo 874

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 199  df-or 875

This theorem is referenced by:  pm4.25  930  orordi  953  orordir  954  truortru  1691  falorfal  1694  unidm  3958  dfsn2ALT  4392  preqsnd  4581  preqsndOLD  4582  preqsnOLD  4586  suceloni  7251  tz7.48lem  7779  msq0i  10970  msq0d  10972  prmdvdsexp  15764  metn0  22497  rrxcph  23522  nb3grprlem2  26629  pdivsq  32153  pm11.7  39382