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

Theorem oridm 494
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 493 . 2  |-  ( (
ph  \/  ph )  ->  ph )
2 pm2.07 383 . 2  |-  ( ph  ->  ( ph  \/  ph ) )
31, 2impbii 178 1  |-  ( (
ph  \/  ph )  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 174    \/ wo 355
This theorem is referenced by:  pm4.25  495  orordi  510  orordir  511  truortru  1275  falorfal  1278  unidm  2945  preqsn  3403  suceloni  4181  tz7.48lem  5918  msq0i  8822  msq0d  8824  prmdvdsexp  11918  metn0  16632  pdivsq  21995  pm11.7  25469
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 175  df-or 357
  Copyright terms: Public domain W3C validator