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

Theorem oridm 514
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 513 . 2  |-  ( (
ph  \/  ph )  ->  ph )
2 pm2.07 396 . 2  |-  ( ph  ->  ( ph  \/  ph ) )
31, 2impbii 188 1  |-  ( (
ph  \/  ph )  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 368
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 370
This theorem is referenced by:  pm4.25  515  orordi  530  orordir  531  truortru  1397  falorfal  1400  unidm  3518  preqsn  4074  suceloni  6443  tz7.48lem  6915  msq0i  10002  msq0d  10004  prmdvdsexp  13819  metn0  19954  rrxcph  20915  nb3graprlem2  23379  preqsnd  25920  pdivsq  27574  nofulllem5  27866  pm11.7  29672
  Copyright terms: Public domain W3C validator