Theorem oridm 904

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

Syntax hints:   ↔ wb 206   ∨ wo 847

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 848

This theorem is referenced by:  pm4.25  905  orordi  928  orordir  929  nornot  1532  truortru  1578  falorfal  1581  unidm  4107  dfsn2ALT  4600  preqsnd  4813  tz7.48lem  8370  msq0i  11784  msq0d  11785  prmdvdsexp  16640  metn0  24302  rrxcph  25346  nb3grprlem2  29403  pm11.7  44579  euoreqb  47297