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 212	1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 209   ∨ 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 210  df-or 845

This theorem is referenced by:  pm4.25  903  orordi  926  orordir  927  nornot  1525  truortru  1575  falorfal  1578  unidm  4079  dfsn2ALT  4545  preqsnd  4749  suceloni  7508  tz7.48lem  8060  msq0i  11276  msq0d  11278  prmdvdsexp  16049  metn0  22967  rrxcph  23996  nb3grprlem2  27171  pdivsq  33094  pm11.7  41100  euoreqb  43665