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  3318  preqsn  3792  suceloni  4604  tz7.48lem  6453  msq0i  9415  msq0d  9417  prmdvdsexp  12793  metn0  17924  preqsnd  23194  pdivsq  24102  nofulllem5  24360  pm11.7  27595
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