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

Theorem orc 374
Description: Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
orc  |-  ( ph  ->  ( ph  \/  ps ) )

Proof of Theorem orc
StepHypRef Expression
1 pm2.24 101 . 2  |-  ( ph  ->  ( -.  ph  ->  ps ) )
21orrd 367 1  |-  ( ph  ->  ( ph  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357
This theorem is referenced by:  pm1.4  375  orcd  381  orcs  383  pm2.45  386  pm2.67-2  391  biorfi  396  pm1.5  508  pm2.4  558  pm4.44  560  pm4.45  669  pm3.48  806  orabs  828  andi  837  pm4.72  846  biort  866  pm5.71  902  dedlema  920  consensus  925  3mix1  1124  cad1  1388  cad11  1389  cad0  1390  19.33  1597  19.33b  1598  dfsb2  2008  moor  2209  ssun1  3351  undif3  3442  reuun1  3463  opthpr  3806  pwundifOLD  4317  elelsuc  4480  trsuc2OLD  4493  ordelinel  4507  ordssun  4508  ordequn  4509  soxp  6244  omopth2  6598  swoord1  6705  swoord2  6706  sornom  7919  fin56  8035  fpwwe2lem12  8279  ltle  8926  nn1m1nn  9782  elnnz  10050  elnn0z  10052  zmulcl  10082  ltpnf  10479  xrltle  10499  xrltne  10510  4sqlem17  13024  funcres2c  13791  tsrlemax  14345  odlem1  14866  gexlem1  14906  drngmuleq0  15551  alexsubALTlem3  17759  dyadmbl  18971  bcmono  20532  dfon2lem4  24213  sltsgn1  24386  sltsgn2  24387  dfrdg4  24560  btwnconn1  24796  segcon2  24800  broutsideof2  24817  lineunray  24842  meran1  24922  dissym1  24932  nxtor  25088  imunt  25100  evpexun  25101  untind  25121  hdrmp  25809  partarelt1  25999  fnwe2lem3  27252  19.33-2  27683  notatnand  27967  abnotataxb  27988  nbusgra  28277  nb3graprlem1  28287  a9e2ndeq  28624  uunT1  28869  undif3VD  28974  a9e2ndeqVD  29001  a9e2ndeqALT  29024  dfsb2NEW7  29609  lkrlspeqN  29983
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 177  df-or 359
  Copyright terms: Public domain W3C validator