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

Theorem olc 373
Description: Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
olc  |-  ( ph  ->  ( ps  \/  ph ) )

Proof of Theorem olc
StepHypRef Expression
1 ax-1 5 . 2  |-  ( ph  ->  ( -.  ps  ->  ph ) )
21orrd 367 1  |-  ( ph  ->  ( ps  \/  ph ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357
This theorem is referenced by:  pm1.4  375  pm2.07  385  pm2.46  387  biorf  394  pm1.5  508  pm2.41  556  jaob  758  pm3.48  806  andi  837  pm4.72  846  dedlemb  921  consensus  925  cad1  1388  19.33  1597  19.33b  1598  dfsb2  2008  mooran2  2211  euor2  2224  undif3  3442  undif4  3524  ordelinel  4507  ordssun  4508  ordequn  4509  frxp  6241  omopth2  6598  swoord1  6705  swoord2  6706  sucprcreg  7329  rankxplim3  7567  fpwwe2lem12  8279  ltapr  8685  zmulcl  10082  elnn1uz2  10310  mnflt  10480  mnfltpnf  10481  expeq0  11148  vdwlem9  13052  funcres2c  13791  tsrlemax  14345  odlem1  14866  gexlem1  14906  0top  16737  cmpfi  17151  alexsubALTlem3  17759  dyadmbl  18971  plydivex  19693  scvxcvx  20296  dfon2lem4  24213  sltsgn1  24386  sltsgn2  24387  dfrdg4  24560  broutsideof2  24817  lineunray  24842  meran1  24922  facrm  25056  nxtor  25088  partarelt1  25999  prtlem90  26826  19.33-2  27683  stoweidlem26  27878  stoweidlem37  27889  nb3graprlem1  28287  uvtx01vtx  28305  1to3vfriswmgra  28431  a9e2ndeq  28624  undif3VD  28974  a9e2ndeqVD  29001  a9e2ndeqALT  29024  dfsb2NEW7  29609  paddclN  30653  lcfl6  32312
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