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  1332  falorfal  1335  unidm  3319  preqsn  3793  suceloni  4603  tz7.48lem  6448  msq0i  9410  msq0d  9412  prmdvdsexp  12787  metn0  17918  pdivsq  23505  pm11.7  26994
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