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

Theorem oridm 534
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 533 . 2 ((𝜑𝜑) → 𝜑)
2 pm2.07 409 . 2 (𝜑 → (𝜑𝜑))
31, 2impbii 197 1 ((𝜑𝜑) ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wo 381
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 195  df-or 383
This theorem is referenced by:  pm4.25  535  orordi  550  orordir  551  truortru  1500  falorfal  1503  unidm  3717  preqsnd  4325  preqsn  4326  preqsnOLD  4327  suceloni  6883  tz7.48lem  7401  msq0i  10526  msq0d  10528  prmdvdsexp  15214  metn0  21923  rrxcph  22933  nb3graprlem2  25775  pdivsq  30722  nofulllem5  30939  pm11.7  37442  nb3grprlem2  40631
  Copyright terms: Public domain W3C validator