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

Theorem olc 375
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 7 . 2  |-  ( ph  ->  ( -.  ps  ->  ph ) )
21orrd 369 1  |-  ( ph  ->  ( ps  \/  ph ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    \/ wo 359
This theorem is referenced by:  pm1.4  377  pm2.07  387  pm2.46  389  biorf  396  pm1.5  510  pm2.41  558  jaob  760  pm3.48  808  andi  839  pm4.72  848  dedlemb  923  consensus  927  cad1  1390  19.33  1595  19.33b  1596  dfsb2  1994  mooran2  2199  euor2  2212  undif3  3430  undif4  3512  ordelinel  4490  ordssun  4491  ordequn  4492  frxp  6186  omopth2  6577  swoord1  6684  swoord2  6685  sucprcreg  7308  rankxplim3  7546  fpwwe2lem12  8258  ltapr  8664  zmulcl  10061  elnn1uz2  10289  mnflt  10459  mnfltpnf  10460  expeq0  11126  vdwlem9  13030  funcres2c  13769  tsrlemax  14323  odlem1  14844  gexlem1  14884  0top  16715  cmpfi  17129  alexsubALTlem3  17737  dyadmbl  18949  plydivex  19671  scvxcvx  20274  dfon2lem4  23543  sltsgn1  23715  sltsgn2  23716  dfrdg4  23895  broutsideof2  24152  lineunray  24177  meran1  24257  facrm  24351  nxtor  24383  partarelt1  25295  prtlem90  26122  19.33-2  26979  stoweidlem26  27174  stoweidlem37  27185  a9e2ndeq  27596  undif3VD  27926  a9e2ndeqVD  27953  a9e2ndeqALT  27976  paddclN  29298  lcfl6  30957
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