Theorem oridm 902

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

Syntax hints:   ↔ wb 205   ∨ wo 844

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 845

This theorem is referenced by:  pm4.25  903  orordi  926  orordir  927  nornot  1529  truortru  1576  falorfal  1579  unidm  4086  dfsn2ALT  4581  preqsnd  4789  sucexeloni  7658  suceloniOLD  7660  tz7.48lem  8272  msq0i  11622  msq0d  11624  prmdvdsexp  16420  prmdvdssqOLD  16424  metn0  23513  rrxcph  24556  nb3grprlem2  27748  pm11.7  42014  euoreqb  44601