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  1558  truortru  1604  falorfal  1607  unidm  4119  dfsn2ALT  4616  preqsnd  4828  tz7.48lem  8427  msq0i  11862  msq0d  11863  prmdvdsexp  16773  metn0  24485  rrxcph  25519  nb3grprlem2  29671  pm11.7  44997  euoreqb  47734