Theorem oridm 901

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

Syntax hints:   ↔ wb 205   ∨ wo 843

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 844

This theorem is referenced by:  pm4.25  902  orordi  925  orordir  926  nornot  1526  truortru  1576  falorfal  1579  unidm  4082  dfsn2ALT  4578  preqsnd  4786  suceloni  7635  tz7.48lem  8242  msq0i  11552  msq0d  11554  prmdvdsexp  16348  prmdvdssqOLD  16352  metn0  23421  rrxcph  24461  nb3grprlem2  27651  pm11.7  41903  euoreqb  44488