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

Theorem oridm 495
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 494 . 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  496  orordi  511  orordir  512  truortru  1281  falorfal  1284  unidm  2977  preqsn  3437  suceloni  4215  tz7.48lem  5952  msq0i  8856  msq0d  8858  prmdvdsexp  11952  metn0  16666  pdivsq  22030  pm11.7  25531
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