Theorem oridm 917

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 916	. 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑)
2		pm2.07 915	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑))
3	1, 2	impbii 212	1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 209   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  pm4.25  918  orordi  941  orordir  942  nornot  1561  truortru  1607  falorfal  1610  unidm  4111  dfsn2ALT  4611  preqsnd  4824  tz7.48lem  8424  msq0i  11858  msq0d  11859  prmdvdsexp  16769  metn0  24517  rrxcph  25551  nb3grprlem2  29731  pm11.7  45106  euoreqb  47846