Theorem oridm 752

Description: Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-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 751	. 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑)
2		pm2.07 732	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑))
3	1, 2	impbii 125	1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 104   ∨ wo 703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.25  753  orordi  768  orordir  769  truortru  1400  falorfal  1403  truxortru  1414  falxorfal  1417  unidm  3270  preqsn  3762  reapirr  8496  reapti  8498  lt2msq  8802  nn0ge2m1nn  9195  absext  11027  prmdvdsexp  12102  sqpweven  12129  2sqpwodd  12130