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  1531  truortru  1577  falorfal  1580  unidm  4137  dfsn2ALT  4628  preqsnd  4840  sucexeloniOLD  7809  suceloniOLD  7811  tz7.48lem  8460  msq0i  11889  msq0d  11891  prmdvdsexp  16739  metn0  24304  rrxcph  25349  nb3grprlem2  29365  pm11.7  44387  euoreqb  47105