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

Theorem orc 376
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 103 . 2  |-  ( ph  ->  ( -.  ph  ->  ps ) )
21orrd 369 1  |-  ( ph  ->  ( ph  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    \/ wo 359
This theorem is referenced by:  pm1.4  377  orcd  383  orcs  385  pm2.45  388  pm2.67-2  393  biorfi  398  pm1.5  510  pm2.4  560  pm4.44  562  pm4.45  671  pm3.48  808  orabs  830  andi  839  pm4.72  848  biort  868  pm5.71  904  dedlema  922  consensus  927  3mix1  1126  cad1  1390  cad11  1391  cad0  1392  19.33  1595  19.33b  1596  dfsb2  1994  moor  2197  ssun1  3339  undif3  3430  reuun1  3451  opthpr  3791  pwundifOLD  4300  elelsuc  4463  trsuc2OLD  4476  ordelinel  4490  ordssun  4491  ordequn  4492  soxp  6189  omopth2  6577  swoord1  6684  swoord2  6685  sornom  7898  fin56  8014  fpwwe2lem12  8258  ltle  8905  nn1m1nn  9761  elnnz  10029  elnn0z  10031  zmulcl  10061  ltpnf  10458  xrltle  10478  xrltne  10489  4sqlem17  13002  funcres2c  13769  tsrlemax  14323  odlem1  14844  gexlem1  14884  drngmuleq0  15529  alexsubALTlem3  17737  dyadmbl  18949  bcmono  20510  dfon2lem4  23543  sltsgn1  23715  sltsgn2  23716  dfrdg4  23895  btwnconn1  24131  segcon2  24135  broutsideof2  24152  lineunray  24177  meran1  24257  dissym1  24267  nxtor  24383  imunt  24395  evpexun  24396  untind  24416  hdrmp  25105  partarelt1  25295  fnwe2lem3  26548  19.33-2  26979  notatnand  27243  abnotataxb  27264  a9e2ndeq  27596  uunT1  27823  undif3VD  27926  a9e2ndeqVD  27953  a9e2ndeqALT  27976  lkrlspeqN  28628
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-or 361
  Copyright terms: Public domain W3C validator