Theorem oridm 905

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 904	. 2 ⊢ ((𝜑 ∨ 𝜑) → 𝜑)
2		pm2.07 903	. 2 ⊢ (𝜑 → (𝜑 ∨ 𝜑))
3	1, 2	impbii 209	1 ⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 206   ∨ wo 848

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 207  df-or 849

This theorem is referenced by:  pm4.25  906  orordi  929  orordir  930  nornot  1533  truortru  1579  falorfal  1582  unidm  4098  dfsn2ALT  4590  preqsnd  4803  tz7.48lem  8374  msq0i  11793  msq0d  11794  prmdvdsexp  16679  metn0  24338  rrxcph  25372  nb3grprlem2  29467  pm11.7  44844  euoreqb  47572