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

Theorem oridm 535
 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 534 . 2 ((𝜑𝜑) → 𝜑)
2 pm2.07 410 . 2 (𝜑 → (𝜑𝜑))
31, 2impbii 199 1 ((𝜑𝜑) ↔ 𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∨ wo 382 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 197  df-or 384 This theorem is referenced by:  pm4.25  536  orordi  551  orordir  552  truortru  1550  falorfal  1553  unidm  3789  preqsnd  4423  preqsn  4424  preqsnOLD  4425  suceloni  7055  tz7.48lem  7581  msq0i  10712  msq0d  10714  prmdvdsexp  15474  metn0  22212  rrxcph  23226  nb3grprlem2  26327  pdivsq  31761  pm11.7  38913
 Copyright terms: Public domain W3C validator