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  4467  prel12g  4865  ordssun  6467  tpres  7202  frxp  8112  frxp2  8130  frxp3  8137  omopth2  8584  naddunif  8692  swoord1  8734  swoord2  8735  fpwwe2lem11  10636  ltapr  11040  zmulcl  12611  nn0lt2  12625  elnn1uz2  12909  mnflt  13103  mnfltpnf  13106  fzm1  13581  expeq0  14058  zzlesq  14170  swrdnnn0nd  14606  nn0o1gt2  16324  prm23lt5  16747  vdwlem9  16922  cshwshashlem1  17029  cshwshash  17038  funcres2c  17852  tsrlemax  18539  odlem1  19403  gexlem1  19447  0top  22486  cmpfi  22912  alexsubALTlem3  23553  dyadmbl  25117  plydivex  25810  scvxcvx  26490  gausslemma2dlem0f  26864  nb3grprlem1  28637  1to3vfriswmgr  29533  frgrwopreg  29576  frgrregorufr  29578  frgrregord13  29649  disjunsn  31825  dfon2lem4  34758  dfrdg4  34923  broutsideof2  35094  lineunray  35119  fwddifnp1  35137  meran1  35296  bj-orim2  35432  bj-peircecurry  35434  bj-falor2  35463  bj-sbsb  35715  bj-unrab  35806  wl-orel12  36380  tsor3  37017  paddclN  38713  lcfl6  40371  sbor2  41028  fsuppind  41162  omcl3g  42084  ifpid3g  42243  ifpim4  42249  rp-fakeanorass  42264  sqrtcval  42392  iunrelexp0  42453  clsk1indlem3  42794  19.33-2  43141  ax6e2ndeq  43320  undif3VD  43643  ax6e2ndeqVD  43670  ax6e2ndeqALT  43692  stoweidlem26  44742  stoweidlem37  44753  fourierswlem  44946  fouriersw  44947  elaa2lem  44949  salexct  45050  sge0z  45091  nfunsnafv2  45933  prproropf1olem4  46174  sfprmdvdsmersenne  46271  nn0o1gt2ALTV  46362  odd2prm2  46386  even3prm2  46387  stgoldbwt  46444  nrhmzr  46647  reorelicc  47396  rrx2plord2  47408  line2y  47441