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  561  pm4.44  563  pm4.45  672  pm3.48  809  orabs  831  andi  842  pm4.72  851  biort  871  pm5.71  907  dedlema  925  consensus  930  3mix1  1129  cad1  1394  cad11  1395  cad0  1396  19.33  1606  19.33b  1607  dfsb2  1947  moor  2166  ssun1  3248  undif3  3336  reuun1  3357  opthpr  3690  pwundifOLD  4194  elelsuc  4357  trsuc2OLD  4370  ordssun  4383  ordequn  4384  soxp  6080  omopth2  6468  swoord1  6575  swoord2  6576  sornom  7787  fin56  7903  fpwwe2lem12  8143  ltle  8790  nn1m1nn  9646  elnnz  9913  elnn0z  9915  zmulcl  9945  ltpnf  10342  xrltle  10362  xrltne  10373  4sqlem17  12882  funcres2c  13619  tsrlemax  14164  odlem1  14685  gexlem1  14725  drngmuleq0  15370  alexsubALTlem3  17575  dyadmbl  18787  bcmono  20348  dfon2lem4  23310  sltsgn1  23482  sltsgn2  23483  dfrdg4  23662  btwnconn1  23898  segcon2  23902  broutsideof2  23919  lineunray  23944  meran1  24024  dissym1  24034  nxtor  24150  imunt  24162  evpexun  24163  untind  24183  hdrmp  24872  partarelt1  25062  fnwe2lem3  26315  19.33-2  26746  a9e2ndeq  27018  uunT1  27245  undif3VD  27348  a9e2ndeqVD  27375  a9e2ndeqALT  27398  lkrlspeqN  28050
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