Theorem olc 384

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

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 |- ( ph -> ( -. ps -> ph ) )
2	1	orrd 378	1 |- ( ph -> ( ps \/ ph ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-or 370

This theorem is referenced by:  pm1.4  386  pm2.07  396  pm2.46  398  biorf  405  pm1.5  522  pm2.41  573  jaob  781  pm3.48  829  norbi  855  andi  862  pm4.72  871  dedlemb  946  consensus  950  cad1  1440  19.33  1662  19.33b  1663  dfsb2  2064  euor2OLD  2313  mooran2  2329  undif3  3632  undif4  3756  ordelinel  4838  ordssun  4839  ordequn  4840  frxp  6703  omopth2  7044  swoord1  7151  swoord2  7152  sucprcregOLD  7836  rankxplim3  8109  fpwwe2lem12  8829  ltapr  9235  zmulcl  10714  elnn1uz2  10952  mnflt  11125  mnfltpnf  11127  expeq0  11915  vdwlem9  14071  cshwshashlem1  14143  cshwshash  14152  funcres2c  14832  tsrlemax  15411  odlem1  16059  gexlem1  16099  0top  18610  cmpfi  19033  alexsubALTlem3  19643  dyadmbl  21102  plydivex  21785  scvxcvx  22401  nb3graprlem1  23381  uvtx01vtx  23422  disjunsn  25958  dfon2lem4  27621  sltsgn1  27824  sltsgn2  27825  dfrdg4  28003  broutsideof2  28175  lineunray  28200  meran1  28279  tsan3  28980  tsor3  28986  prtlem90  29028  19.33-2  29660  stoweidlem26  29847  stoweidlem37  29858  nn0lt2  30212  1to3vfriswmgra  30625  frgraregorufr  30672  frgraregord13  30738  ax6e2ndeq  31364  undif3VD  31714  ax6e2ndeqVD  31741  ax6e2ndeqALT  31763  bj-dfif5ALT  32182  bj-anif  32190  bj-falor2  32207  bj-nfntht  32232  bj-nfntht2  32233  bj-unrab  32525  paddclN  33582  lcfl6  35241