Theorem oridm 903

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

Syntax hints:   ↔ wb 205   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  pm4.25  904  orordi  927  orordir  928  nornot  1525  truortru  1571  falorfal  1574  unidm  4151  dfsn2ALT  4649  preqsnd  4860  sucexeloniOLD  7813  suceloniOLD  7815  tz7.48lem  8462  msq0i  11892  msq0d  11894  prmdvdsexp  16686  prmdvdssqOLD  16690  metn0  24279  rrxcph  25333  nb3grprlem2  29207  pm11.7  43833  euoreqb  46489