MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oridm Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 pm1.2 901 . 2 ((𝜑𝜑) → 𝜑)
2 pm2.07 900 . 2 (𝜑 → (𝜑𝜑))
31, 2impbii 208 1 ((𝜑𝜑) ↔ 𝜑)
Colors of variables: wff setvar class
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  1579  falorfal  1582  unidm  4091  dfsn2ALT  4587  preqsnd  4795  sucexeloni  7652  suceloniOLD  7654  tz7.48lem  8263  msq0i  11622  msq0d  11624  prmdvdsexp  16418  prmdvdssqOLD  16422  metn0  23511  rrxcph  24554  nb3grprlem2  27746  pm11.7  41984  euoreqb  44569
  Copyright terms: Public domain W3C validator