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

Theorem oridm 501
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 500 . 2  |-  ( (
ph  \/  ph )  ->  ph )
2 pm2.07 386 . 2  |-  ( ph  ->  ( ph  \/  ph ) )
31, 2impbii 181 1  |-  ( (
ph  \/  ph )  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    \/ wo 358
This theorem is referenced by:  pm4.25  502  orordi  517  orordir  518  truortru  1346  falorfal  1349  unidm  3450  preqsn  3940  suceloni  4752  tz7.48lem  6657  msq0i  9625  msq0d  9627  prmdvdsexp  13069  metn0  18343  nb3graprlem2  21414  preqsnd  23953  pdivsq  25316  nofulllem5  25574  pm11.7  27463
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 178  df-or 360
  Copyright terms: Public domain W3C validator