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  3279  preqsn  3752  suceloni  4562  tz7.48lem  6407  msq0i  9369  msq0d  9371  prmdvdsexp  12741  metn0  17872  pdivsq  23459  pm11.7  26948
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