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 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  905  orordi  928  orordir  929  nornot  1533  truortru  1579  falorfal  1582  unidm  4153  dfsn2ALT  4649  preqsnd  4860  sucexeloniOLD  7798  suceloniOLD  7800  tz7.48lem  8441  msq0i  11861  msq0d  11863  prmdvdsexp  16652  prmdvdssqOLD  16656  metn0  23866  rrxcph  24909  nb3grprlem2  28638  pm11.7  43155  euoreqb  45817