Theorem olc 867

Description: Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
olc	⊢ (𝜑 → (𝜓 ∨ 𝜑))

Proof of Theorem olc

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜑))
2	1	orrd 862	1 ⊢ (𝜑 → (𝜓 ∨ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  pm1.4  868  pm2.46  882  norbi  886  pm2.07  902  pm2.41  907  pm1.5  919  biorf  936  pm4.72  949  jaob  961  pm3.48  963  andi  1007  dedlemb  1046  consensus  1052  anifp  1071  cad1  1619  19.33  1888  19.33b  1889  dfsb2  2493  mooran2  2551  undif4  4466  prel12g  4864  ordssun  6464  tpres  7199  frxp  8109  frxp2  8127  frxp3  8134  omopth2  8581  naddunif  8689  swoord1  8731  swoord2  8732  fpwwe2lem11  10633  ltapr  11037  zmulcl  12608  nn0lt2  12622  elnn1uz2  12906  mnflt  13100  mnfltpnf  13103  fzm1  13578  expeq0  14055  zzlesq  14167  swrdnnn0nd  14603  nn0o1gt2  16321  prm23lt5  16744  vdwlem9  16919  cshwshashlem1  17026  cshwshash  17035  funcres2c  17849  tsrlemax  18536  odlem1  19398  gexlem1  19442  0top  22478  cmpfi  22904  alexsubALTlem3  23545  dyadmbl  25109  plydivex  25802  scvxcvx  26480  gausslemma2dlem0f  26854  nb3grprlem1  28627  1to3vfriswmgr  29523  frgrwopreg  29566  frgrregorufr  29568  frgrregord13  29639  disjunsn  31813  dfon2lem4  34747  dfrdg4  34912  broutsideof2  35083  lineunray  35108  fwddifnp1  35126  meran1  35285  bj-orim2  35421  bj-peircecurry  35423  bj-falor2  35452  bj-sbsb  35704  bj-unrab  35795  wl-orel12  36369  tsor3  37006  paddclN  38702  lcfl6  40360  sbor2  41024  fsuppind  41160  omcl3g  42070  ifpid3g  42229  ifpim4  42235  rp-fakeanorass  42250  sqrtcval  42378  iunrelexp0  42439  clsk1indlem3  42780  19.33-2  43127  ax6e2ndeq  43306  undif3VD  43629  ax6e2ndeqVD  43656  ax6e2ndeqALT  43678  stoweidlem26  44729  stoweidlem37  44740  fourierswlem  44933  fouriersw  44934  elaa2lem  44936  salexct  45037  sge0z  45078  nfunsnafv2  45920  prproropf1olem4  46161  sfprmdvdsmersenne  46258  nn0o1gt2ALTV  46349  odd2prm2  46373  even3prm2  46374  stgoldbwt  46431  nrhmzr  46634  reorelicc  47350  rrx2plord2  47362  line2y  47395