Theorem oridm 904

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

Syntax hints:   ↔ wb 206   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  pm4.25  905  orordi  928  orordir  929  nornot  1528  truortru  1574  falorfal  1577  unidm  4167  dfsn2ALT  4652  preqsnd  4864  sucexeloniOLD  7830  suceloniOLD  7832  tz7.48lem  8480  msq0i  11908  msq0d  11910  prmdvdsexp  16749  metn0  24386  rrxcph  25440  nb3grprlem2  29413  pm11.7  44392  euoreqb  47059