Theorem oridm 535

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

Syntax hints:   ↔ wb 195   ∨ wo 382

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-or 384

This theorem is referenced by:  pm4.25  536  orordi  551  orordir  552  truortru  1501  falorfal  1504  unidm  3718  preqsnd  4330  preqsn  4331  preqsnOLD  4332  suceloni  6905  tz7.48lem  7423  msq0i  10553  msq0d  10555  prmdvdsexp  15265  metn0  21975  rrxcph  22988  nb3graprlem2  25981  pdivsq  30888  nofulllem5  31105  pm11.7  37618  nb3grprlem2  40609