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

Theorem oridm 502
Description: Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 16-Apr-2011.) (Proof shortened by Wolf Lammen, 10-Mar-2013.)
Assertion
Ref Expression
oridm  |-  ( (
ph  \/  ph )  <->  ph )

Proof of Theorem oridm
StepHypRef Expression
1 pm1.2 501 . 2  |-  ( (
ph  \/  ph )  ->  ph )
2 pm2.07 387 . 2  |-  ( ph  ->  ( ph  \/  ph ) )
31, 2impbii 182 1  |-  ( (
ph  \/  ph )  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    \/ wo 359
This theorem is referenced by:  pm4.25  503  orordi  518  orordir  519  truortru  1336  falorfal  1339  unidm  3225  preqsn  3689  suceloni  4492  tz7.48lem  6336  msq0i  9273  msq0d  9275  prmdvdsexp  12629  metn0  17718  pdivsq  23203  pm11.7  26692
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-or 361
  Copyright terms: Public domain W3C validator