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  1594  19.33b  1595  dfsb2  1995  moor  2196  ssun1  3338  undif3  3429  reuun1  3450  opthpr  3790  pwundifOLD  4301  elelsuc  4464  trsuc2OLD  4477  ordelinel  4491  ordssun  4492  ordequn  4493  soxp  6228  omopth2  6582  swoord1  6689  swoord2  6690  sornom  7903  fin56  8019  fpwwe2lem12  8263  ltle  8910  nn1m1nn  9766  elnnz  10034  elnn0z  10036  zmulcl  10066  ltpnf  10463  xrltle  10483  xrltne  10494  4sqlem17  13008  funcres2c  13775  tsrlemax  14329  odlem1  14850  gexlem1  14890  drngmuleq0  15535  alexsubALTlem3  17743  dyadmbl  18955  bcmono  20516  dfon2lem4  24142  sltsgn1  24315  sltsgn2  24316  dfrdg4  24488  btwnconn1  24724  segcon2  24728  broutsideof2  24745  lineunray  24770  meran1  24850  dissym1  24860  nxtor  24985  imunt  24997  evpexun  24998  untind  25018  hdrmp  25706  partarelt1  25896  fnwe2lem3  27149  19.33-2  27580  notatnand  27864  abnotataxb  27885  nbusgra  28143  a9e2ndeq  28325  uunT1  28555  undif3VD  28658  a9e2ndeqVD  28685  a9e2ndeqALT  28708  lkrlspeqN  29361
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