Theorem oridm 747

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 746	. 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑)
2		pm2.07 727	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑))
3	1, 2	impbii 125	1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 104   ∨ wo 698

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 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.25  748  orordi  763  orordir  764  truortru  1395  falorfal  1398  truxortru  1409  falxorfal  1412  unidm  3265  preqsn  3755  reapirr  8475  reapti  8477  lt2msq  8781  nn0ge2m1nn  9174  absext  11005  prmdvdsexp  12080  sqpweven  12107  2sqpwodd  12108