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

Theorem oridm 929
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 928 . 2 ((𝜑𝜑) → 𝜑)
2 pm2.07 927 . 2 (𝜑 → (𝜑𝜑))
31, 2impbii 201 1 ((𝜑𝜑) ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 198  wo 874
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 199  df-or 875
This theorem is referenced by:  pm4.25  930  orordi  953  orordir  954  truortru  1691  falorfal  1694  unidm  3958  dfsn2ALT  4392  preqsnd  4581  preqsndOLD  4582  preqsnOLD  4586  suceloni  7251  tz7.48lem  7779  msq0i  10970  msq0d  10972  prmdvdsexp  15764  metn0  22497  rrxcph  23522  nb3grprlem2  26629  pdivsq  32153  pm11.7  39382
  Copyright terms: Public domain W3C validator