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

Theorem oridm 900
 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 899 . 2 ((𝜑𝜑) → 𝜑)
2 pm2.07 898 . 2 (𝜑 → (𝜑𝜑))
31, 2impbii 211 1 ((𝜑𝜑) ↔ 𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 208   ∨ wo 843 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 209  df-or 844 This theorem is referenced by:  pm4.25  901  orordi  924  orordir  925  nornot  1517  truortru  1567  falorfal  1570  unidm  4126  dfsn2ALT  4579  preqsnd  4781  suceloni  7520  tz7.48lem  8069  msq0i  11279  msq0d  11281  prmdvdsexp  16051  metn0  22962  rrxcph  23987  nb3grprlem2  27155  pdivsq  32969  pm11.7  40713  euoreqb  43293
 Copyright terms: Public domain W3C validator