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 846

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 847

This theorem is referenced by:  pm4.25  904  orordi  927  orordir  928  nornot  1525  truortru  1571  falorfal  1574  unidm  4148  dfsn2ALT  4644  preqsnd  4855  sucexeloniOLD  7805  suceloniOLD  7807  tz7.48lem  8453  msq0i  11877  msq0d  11879  prmdvdsexp  16671  prmdvdssqOLD  16675  metn0  24240  rrxcph  25294  nb3grprlem2  29168  pm11.7  43746  euoreqb  46402