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

Theorem oridm 500
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 499 . 2  |-  ( (
ph  \/  ph )  ->  ph )
2 pm2.07 385 . 2  |-  ( ph  ->  ( ph  \/  ph ) )
31, 2impbii 180 1  |-  ( (
ph  \/  ph )  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357
This theorem is referenced by:  pm4.25  501  orordi  516  orordir  517  truortru  1330  falorfal  1333  unidm  3331  preqsn  3808  suceloni  4620  tz7.48lem  6469  msq0i  9431  msq0d  9433  prmdvdsexp  12809  metn0  17940  preqsnd  23209  pdivsq  24172  nofulllem5  24430  pm11.7  27697  nb3graprlem2  28287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
  Copyright terms: Public domain W3C validator