Theorem olc 882

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm1.4  883  pm2.46  896  norbi  900  pm2.07  916  pm2.41  921  pm1.5  933  biorf  950  pm4.72  964  jaob  976  pm3.48  978  andi  1025  dedlemb  1062  consensus  1068  anifp  1088  cad1  1650  19.33  1917  19.33b  1918  dfsb2  2524  mooran2  2583  undif4  4423  prel12g  4827  ordssun  6466  tpres  7203  fvf1pr  7311  frxp  8127  frxp2  8145  frxp3  8152  omopth2  8574  naddunif  8685  swoord1  8732  swoord2  8733  fpwwe2lem11  10653  ltapr  11057  zmulcl  12670  nn0lt2  12687  elnn1uz2  12977  mnflt  13176  mnfltpnf  13179  fzm1  13664  expeq0  14158  zzlesq  14272  swrdnnn0nd  14728  nn0o1gt2  16475  prm23lt5  16910  vdwlem9  17085  cshwshashlem1  17191  cshwshash  17200  funcres2c  17996  tsrlemax  18678  odlem1  19663  gexlem1  19707  nrhmzr  20700  0top  23209  cmpfi  23634  alexsubALTlem3  24276  dyadmbl  25829  plydivex  26528  scvxcvx  27220  gausslemma2dlem0f  27595  nb3grprlem1  29826  1to3vfriswmgr  30746  frgrwopreg  30789  frgrregorufr  30791  frgrregord13  30862  disjunsn  33054  axprALT2  35604  dfon2lem4  36350  dfrdg4  36517  broutsideof2  36689  lineunray  36714  fwddifnp1  36732  meran1  37017  axtco1from2  37081  bj-orim2  37243  bj-peircecurry  37245  bj-falor2  37273  bj-sbsb  37567  bj-unrab  37657  wl-orel12  38261  tsor3  38884  paddclN  40702  lcfl6  42360  quadfac  43058  sbor2  43067  fsuppind  43423  omcl3g  44162  ifpid3g  44319  ifpim4  44325  rp-fakeanorass  44340  sqrtcval  44468  iunrelexp0  44529  clsk1indlem3  44870  19.33-2  45193  ax6e2ndeq  45369  undif3VD  45691  ax6e2ndeqVD  45718  ax6e2ndeqALT  45740  stoweidlem26  46841  stoweidlem37  46852  fourierswlem  47045  fouriersw  47046  elaa2lem  47048  salexct  47149  sge0z  47190  nfunsnafv2  48100  prproropf1olem4  48393  sfprmdvdsmersenne  48493  nn0o1gt2ALTV  48597  odd2prm2  48621  even3prm2  48622  stgoldbwt  48679  clnbgrel  48731  gpg5nbgrvtx03starlem1  48971  gpg5nbgrvtx03starlem2  48972  gpg5nbgrvtx03starlem3  48973  gpg5nbgrvtx13starlem1  48974  gpg5nbgrvtx13starlem2  48975  gpg5nbgrvtx13starlem3  48976  gpg5edgnedg  49033  reorelicc  49627  rrx2plord2  49639  line2y  49672  opth2neg  49742