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  4465  prel12g  4863  ordssun  6463  tpres  7197  frxp  8107  frxp2  8125  frxp3  8132  omopth2  8580  naddunif  8688  swoord1  8730  swoord2  8731  fpwwe2lem11  10632  ltapr  11036  zmulcl  12607  nn0lt2  12621  elnn1uz2  12905  mnflt  13099  mnfltpnf  13102  fzm1  13577  expeq0  14054  zzlesq  14166  swrdnnn0nd  14602  nn0o1gt2  16320  prm23lt5  16743  vdwlem9  16918  cshwshashlem1  17025  cshwshash  17034  funcres2c  17848  tsrlemax  18535  odlem1  19396  gexlem1  19440  0top  22468  cmpfi  22894  alexsubALTlem3  23535  dyadmbl  25099  plydivex  25792  scvxcvx  26470  gausslemma2dlem0f  26844  nb3grprlem1  28617  1to3vfriswmgr  29513  frgrwopreg  29556  frgrregorufr  29558  frgrregord13  29629  disjunsn  31803  dfon2lem4  34696  dfrdg4  34861  broutsideof2  35032  lineunray  35057  fwddifnp1  35075  meran1  35234  bj-orim2  35370  bj-peircecurry  35372  bj-falor2  35401  bj-sbsb  35653  bj-unrab  35744  wl-orel12  36318  tsor3  36955  paddclN  38651  lcfl6  40309  sbor2  40975  fsuppind  41112  omcl3g  42017  ifpid3g  42176  ifpim4  42182  rp-fakeanorass  42197  sqrtcval  42325  iunrelexp0  42386  clsk1indlem3  42727  19.33-2  43074  ax6e2ndeq  43253  undif3VD  43576  ax6e2ndeqVD  43603  ax6e2ndeqALT  43625  stoweidlem26  44677  stoweidlem37  44688  fourierswlem  44881  fouriersw  44882  elaa2lem  44884  salexct  44985  sge0z  45026  nfunsnafv2  45868  prproropf1olem4  46109  sfprmdvdsmersenne  46206  nn0o1gt2ALTV  46297  odd2prm2  46321  even3prm2  46322  stgoldbwt  46379  nrhmzr  46582  reorelicc  47298  rrx2plord2  47310  line2y  47343