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  8905  reapti  8907  lt2msq  9216  nn0ge2m1nn  9627  absext  11829  prmdvdsexp  12926  sqpweven  12953  2sqpwodd  12954