Theorem oridm 769

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 768	. 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑)
2		pm2.07 749	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑))
3	1, 2	impbii 126	1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)

This proof depends on syntax axioms:   ↔ wb 105   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm4.25  770  orordi  785  orordir  786  truortru  1454  falorfal  1457  truxortru  1468  falxorfal  1471  unidm  3372  preqsn  3900  funopsn  5891  reapirr  8908  reapti  8910  lt2msq  9219  nn0ge2m1nn  9632  absext  11845  prmdvdsexp  12946  sqpweven  12974  2sqpwodd  12975