Theorem oridm 707

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 706	. 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑)
2		pm2.07 689	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑))
3	1, 2	impbii 124	1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 103   ∨ wo 662

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm4.25  708  orordi  723  orordir  724  truortru  1339  falorfal  1342  truxortru  1353  falxorfal  1356  unidm  3132  preqsn  3604  reapirr  7998  reapti  8000  lt2msq  8285  nn0ge2m1nn  8669  absext  10395  prmdvdsexp  11033  sqpweven  11059  2sqpwodd  11060