Theorem oridm 903

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

Syntax hints:   ↔ wb 205   ∨ wo 845

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 846

This theorem is referenced by:  pm4.25  904  orordi  927  orordir  928  nornot  1532  truortru  1578  falorfal  1581  unidm  4151  dfsn2ALT  4647  preqsnd  4858  sucexeloniOLD  7794  suceloniOLD  7796  tz7.48lem  8437  msq0i  11857  msq0d  11859  prmdvdsexp  16648  prmdvdssqOLD  16652  metn0  23857  rrxcph  24900  nb3grprlem2  28627  pm11.7  43140  euoreqb  45803