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 198 1 ((𝜑𝜑) ↔ 𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∨ 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 196  df-or 384 This theorem is referenced by:  pm4.25  536  orordi  551  orordir  552  truortru  1501  falorfal  1504  unidm  3718  preqsnd  4330  preqsn  4331  preqsnOLD  4332  suceloni  6905  tz7.48lem  7423  msq0i  10553  msq0d  10555  prmdvdsexp  15265  metn0  21975  rrxcph  22988  nb3graprlem2  25981  pdivsq  30888  nofulllem5  31105  pm11.7  37618  nb3grprlem2  40609
 Copyright terms: Public domain W3C validator