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  831  norbi  857  andi  865  pm4.72  874  dedlemb  953  consensus  957  cad1  1450  19.33  1672  19.33b  1673  dfsb2  2087  euor2OLD  2335  mooran2  2351  undif3  3759  undif4  3883  ordelinel  4976  ordssun  4977  ordequn  4978  frxp  6893  omopth2  7233  swoord1  7340  swoord2  7341  sucprcregOLD  8026  rankxplim3  8299  fpwwe2lem12  9019  ltapr  9423  zmulcl  10911  nn0lt2  10925  elnn1uz2  11158  mnflt  11333  mnfltpnf  11335  expeq0  12164  vdwlem9  14366  cshwshashlem1  14438  cshwshash  14447  funcres2c  15128  tsrlemax  15707  odlem1  16365  gexlem1  16405  0top  19279  cmpfi  19702  alexsubALTlem3  20312  dyadmbl  21772  plydivex  22455  scvxcvx  23071  nb3graprlem1  24155  uvtx01vtx  24196  1to3vfriswmgra  24711  frgraregorufr  24758  frgraregord13  24824  disjunsn  27154  dfon2lem4  28823  sltsgn1  29026  sltsgn2  29027  dfrdg4  29205  broutsideof2  29377  lineunray  29402  meran1  29481  tsan3  30182  tsor3  30188  prtlem90  30230  19.33-2  30893  sumnnodd  31200  stoweidlem26  31354  stoweidlem37  31365  fourierswlem  31559  fouriersw  31560  ax6e2ndeq  32430  undif3VD  32780  ax6e2ndeqVD  32807  ax6e2ndeqALT  32829  bj-dfif5ALT  33248  bj-anif  33256  bj-falor2  33273  bj-nfntht  33300  bj-nfntht2  33301  bj-unrab  33593  paddclN  34656  lcfl6  36315