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

Theorem olc 374
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 368 1  |-  ( ph  ->  ( ps  \/  ph ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 358
This theorem is referenced by:  pm1.4  376  pm2.07  386  pm2.46  388  biorf  395  pm1.5  509  pm2.41  557  jaob  759  pm3.48  807  andi  838  pm4.72  847  dedlemb  922  consensus  926  cad1  1407  19.33  1617  19.33b  1618  dfsb2  2115  mooran2  2335  euor2  2348  undif3  3589  undif4  3671  ordelinel  4666  ordssun  4667  ordequn  4668  frxp  6442  omopth2  6813  swoord1  6920  swoord2  6921  sucprcreg  7551  rankxplim3  7789  fpwwe2lem12  8500  ltapr  8906  zmulcl  10308  elnn1uz2  10536  mnflt  10706  mnfltpnf  10707  expeq0  11393  vdwlem9  13340  funcres2c  14081  tsrlemax  14635  odlem1  15156  gexlem1  15196  0top  17031  cmpfi  17454  alexsubALTlem3  18063  dyadmbl  19475  plydivex  20197  scvxcvx  20807  nb3graprlem1  21443  uvtx01vtx  21484  dfon2lem4  25392  sltsgn1  25565  sltsgn2  25566  dfrdg4  25740  broutsideof2  25999  lineunray  26024  meran1  26104  prtlem90  26638  19.33-2  27490  stoweidlem26  27684  stoweidlem37  27695  1to3vfriswmgra  28153  frgraregorufr  28198  a9e2ndeq  28399  undif3VD  28746  a9e2ndeqVD  28773  a9e2ndeqALT  28796  dfsb2NEW7  29385  paddclN  30370  lcfl6  32029
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 178  df-or 360
  Copyright terms: Public domain W3C validator