Theorem oridm 536

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 535	. 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑)
2		pm2.07 411	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑))
3	1, 2	impbii 199	1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 196   ∨ wo 383

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 197  df-or 385

This theorem is referenced by:  pm4.25  537  orordi  552  orordir  553  truortru  1510  falorfal  1513  unidm  3756  preqsnd  4392  preqsn  4393  preqsnOLD  4394  suceloni  7013  tz7.48lem  7536  msq0i  10674  msq0d  10676  prmdvdsexp  15427  metn0  22165  rrxcph  23180  nb3grprlem2  26283  pdivsq  31635  pm11.7  38596