Theorem olc 382

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 376	1 |- ( ph -> ( ps \/ ph ) )

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

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 368

This theorem is referenced by:  pm1.4  384  pm2.07  394  pm2.46  396  biorf  403  pm1.5  520  pm2.41  571  jaob  781  pm3.48  831  norbi  857  andi  865  pm4.72  874  dedlemb  953  consensus  957  cad1  1468  cad1OLD  1469  19.33  1700  19.33b  1701  dfsb2  2116  mooran2  2346  undif3  3756  undif4  3871  ordelinel  4965  ordssun  4966  ordequn  4967  tpres  6100  frxp  6883  omopth2  7225  swoord1  7332  swoord2  7333  rankxplim3  8290  fpwwe2lem12  9008  ltapr  9412  zmulcl  10908  nn0lt2  10923  elnn1uz2  11159  mnflt  11336  mnfltpnf  11338  fzm1  11762  expeq0  12178  vdwlem9  14591  cshwshashlem1  14664  cshwshash  14673  funcres2c  15389  tsrlemax  16049  odlem1  16758  gexlem1  16798  0top  19652  cmpfi  20075  alexsubALTlem3  20715  dyadmbl  22175  plydivex  22859  scvxcvx  23513  nb3graprlem1  24653  uvtx01vtx  24694  1to3vfriswmgra  25209  frgraregorufr  25255  frgraregord13  25321  disjunsn  27664  dfon2lem4  29458  sltsgn1  29661  sltsgn2  29662  dfrdg4  29828  broutsideof2  30000  lineunray  30025  meran1  30104  wl-orel12  30209  tsor3  30796  prtlem90  30838  19.33-2  31528  stoweidlem26  32047  stoweidlem37  32058  fourierswlem  32252  fouriersw  32253  elaa2lem  32255  nn0o1gt2ALTV  32600  nrhmzr  32933  nn0o1gt2  33391  ax6e2ndeq  33726  undif3VD  34083  ax6e2ndeqVD  34110  ax6e2ndeqALT  34132  anifp  34559  bj-falor2  34575  bj-nfntht  34600  bj-nfntht2  34601  bj-unrab  34895  paddclN  35963  lcfl6  37624  ifpid3g  38108  ifpim4  38114  rp-fakeanorass  38151  iunrelexp0  38224