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  1948  moor  2169  ssun1  3299  undif3  3390  reuun1  3411  opthpr  3750  pwundifOLD  4259  elelsuc  4422  trsuc2OLD  4435  ordelinel  4449  ordssun  4450  ordequn  4451  soxp  6148  omopth2  6536  swoord1  6643  swoord2  6644  sornom  7857  fin56  7973  fpwwe2lem12  8217  ltle  8864  nn1m1nn  9720  elnnz  9987  elnn0z  9989  zmulcl  10019  ltpnf  10416  xrltle  10436  xrltne  10447  4sqlem17  12956  funcres2c  13723  tsrlemax  14277  odlem1  14798  gexlem1  14838  drngmuleq0  15483  alexsubALTlem3  17691  dyadmbl  18903  bcmono  20464  dfon2lem4  23497  sltsgn1  23669  sltsgn2  23670  dfrdg4  23849  btwnconn1  24085  segcon2  24089  broutsideof2  24106  lineunray  24131  meran1  24211  dissym1  24221  nxtor  24337  imunt  24349  evpexun  24350  untind  24370  hdrmp  25059  partarelt1  25249  fnwe2lem3  26502  19.33-2  26933  notatnand  27139  abnotataxb  27160  a9e2ndeq  27362  uunT1  27589  undif3VD  27692  a9e2ndeqVD  27719  a9e2ndeqALT  27742  lkrlspeqN  28512
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