Theorem olc 868

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 863	1 ⊢ (𝜑 → (𝜓 ∨ 𝜑))

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

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 207  df-or 848

This theorem is referenced by:  pm1.4  869  pm2.46  882  norbi  886  pm2.07  902  pm2.41  907  pm1.5  919  biorf  936  pm4.72  951  jaob  963  pm3.48  965  andi  1009  dedlemb  1046  consensus  1052  anifp  1071  cad1  1618  19.33  1885  19.33b  1886  dfsb2  2493  mooran2  2551  undif4  4414  prel12g  4813  ordssun  6410  tpres  7135  fvf1pr  7241  frxp  8056  frxp2  8074  frxp3  8081  omopth2  8499  naddunif  8608  swoord1  8654  swoord2  8655  fpwwe2lem11  10532  ltapr  10936  zmulcl  12521  nn0lt2  12536  elnn1uz2  12823  mnflt  13022  mnfltpnf  13025  fzm1  13507  expeq0  13999  zzlesq  14113  swrdnnn0nd  14564  nn0o1gt2  16292  prm23lt5  16726  vdwlem9  16901  cshwshashlem1  17007  cshwshash  17016  funcres2c  17810  tsrlemax  18492  odlem1  19447  gexlem1  19491  nrhmzr  20452  0top  22898  cmpfi  23323  alexsubALTlem3  23964  dyadmbl  25528  plydivex  26232  scvxcvx  26923  gausslemma2dlem0f  27299  nb3grprlem1  29358  1to3vfriswmgr  30260  frgrwopreg  30303  frgrregorufr  30305  frgrregord13  30376  disjunsn  32574  dfon2lem4  35828  dfrdg4  35995  broutsideof2  36166  lineunray  36191  fwddifnp1  36209  meran1  36455  bj-orim2  36600  bj-peircecurry  36602  bj-falor2  36629  bj-sbsb  36881  bj-unrab  36970  wl-orel12  37555  tsor3  38188  paddclN  39940  lcfl6  41598  sbor2  42304  fsuppind  42682  omcl3g  43426  ifpid3g  43584  ifpim4  43590  rp-fakeanorass  43605  sqrtcval  43733  iunrelexp0  43794  clsk1indlem3  44135  19.33-2  44474  ax6e2ndeq  44651  undif3VD  44973  ax6e2ndeqVD  45000  ax6e2ndeqALT  45022  stoweidlem26  46123  stoweidlem37  46134  fourierswlem  46327  fouriersw  46328  elaa2lem  46330  salexct  46431  sge0z  46472  nfunsnafv2  47324  prproropf1olem4  47605  sfprmdvdsmersenne  47702  nn0o1gt2ALTV  47793  odd2prm2  47817  even3prm2  47818  stgoldbwt  47875  clnbgrel  47927  gpg5nbgrvtx03starlem1  48167  gpg5nbgrvtx03starlem2  48168  gpg5nbgrvtx03starlem3  48169  gpg5nbgrvtx13starlem1  48170  gpg5nbgrvtx13starlem2  48171  gpg5nbgrvtx13starlem3  48172  gpg5edgnedg  48229  reorelicc  48810  rrx2plord2  48822  line2y  48855  opth2neg  48926