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 199	1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 196   ∨ 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 197  df-or 384

This theorem is referenced by:  pm4.25  536  orordi  551  orordir  552  truortru  1550  falorfal  1553  unidm  3789  preqsnd  4423  preqsn  4424  preqsnOLD  4425  suceloni  7055  tz7.48lem  7581  msq0i  10712  msq0d  10714  prmdvdsexp  15474  metn0  22212  rrxcph  23226  nb3grprlem2  26327  pdivsq  31761  pm11.7  38913