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

Theorem oridm 496
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 495 . 2  |-  ( (
ph  \/  ph )  ->  ph )
2 pm2.07 384 . 2  |-  ( ph  ->  ( ph  \/  ph ) )
31, 2impbii 179 1  |-  ( (
ph  \/  ph )  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 175    \/ wo 356
This theorem is referenced by:  pm4.25  497  orordi  512  orordir  513  truortru  1325  falorfal  1328  unidm  3208  preqsn  3672  suceloni  4474  tz7.48lem  6313  msq0i  9249  msq0d  9251  prmdvdsexp  12601  metn0  17602  pdivsq  23078  pm11.7  26567
This theorem was proved from axioms:  ax-1 6  ax-2 7  ax-3 8  ax-mp 9
This theorem depends on definitions:  df-bi 176  df-or 358
  Copyright terms: Public domain W3C validator