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

Theorem oridm 512
Description: Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-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 511 . 2  |-  ( (
ph  \/  ph )  ->  ph )
2 pm2.07 394 . 2  |-  ( ph  ->  ( ph  \/  ph ) )
31, 2impbii 188 1  |-  ( (
ph  \/  ph )  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 368
This theorem is referenced by:  pm4.25  513  orordi  528  orordir  529  truortru  1426  falorfal  1429  unidm  3633  preqsn  4199  suceloni  6621  tz7.48lem  7098  msq0i  10192  msq0d  10194  prmdvdsexp  14339  metn0  21029  rrxcph  21990  nb3graprlem2  24654  preqsnd  27624  pdivsq  29415  nofulllem5  29706  pm11.7  31543
  Copyright terms: Public domain W3C validator