Theorem jaoi 871

Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.)

Hypotheses

Ref	Expression
jaoi.1	⊢ (𝜑 → 𝜓)
jaoi.2	⊢ (𝜒 → 𝜓)

Assertion

Ref	Expression
jaoi	⊢ ((𝜑 ∨ 𝜒) → 𝜓)

Proof of Theorem jaoi

Step	Hyp	Ref	Expression
1		pm2.53 865	. . 3 ⊢ ((𝜑 ∨ 𝜒) → (¬ 𝜑 → 𝜒))
2		jaoi.2	. . 3 ⊢ (𝜒 → 𝜓)
3	1, 2	syl6 36	. 2 ⊢ ((𝜑 ∨ 𝜒) → (¬ 𝜑 → 𝜓))
4		jaoi.1	. 2 ⊢ (𝜑 → 𝜓)
5	3, 4	pm2.61d2 183	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:  jao1i  872  jaod  873  pm1.4  883  pm3.2ni  894  pm1.2  917  pm2.4  920  pm2.41  921  orim12i  922  pm1.5  933  pm2.42  957  jaoa  970  jaoian  971  pm4.44  1012  andi  1025  ecase3  1048  cases2ALT  1064  consensus  1068  jaoi3  1076  1fpid3  1098  19.33  1919  19.33b  1920  nfim1  2239  dfsb2  2525  mooran1  2583  eueq3  3672  sbcor  3792  sspss  4032  sspsstr  4039  inss  4148  elun  4155  ssun  4196  raaan2  4481  ifbi  4508  ifcomnan  4542  rabsnifsb  4685  tpprceq3  4769  tppreqb  4770  sssn  4787  snsssn  4801  preq12b  4810  prnebg  4816  preq12nebg  4823  elpr2elpr  4829  pwpw0  4836  prproe  4838  3elpr2eq  4839  unissint  4937  zfpair  5390  axprg  5402  propeqop  5486  propssopi  5487  opthhausdorff  5497  opthhausdorff0  5498  iunopeqop  5501  iunopeqopOLD  5502  relsnb  5789  iresn0n0  6064  sotri2  6141  sotri3  6142  somincom  6146  ordssun  6493  unizlim  6513  onxpdisj  6516  tpres  7238  sorpssuni  7780  ordeleqon  7830  ordunisuc  7877  orduninsuc  7888  tfinds  7905  limomss  7916  limom  7927  soxp  8178  ressuppssdif  8240  tfr2b  8442  omopthi  8708  domnsym  9160  ordfin  9269  brwdom  9598  cantnfvalf  9703  ttrclselem1  9763  elhf2  9947  djuss  10038  djuunxp  10039  eldju2ndl  10042  eldju2ndr  10043  djuun  10044  updjud  10052  iscard3  10211  cflim2  10380  sornom  10394  isfin5  10416  isfin6  10417  sdom2en01  10419  fin23lem29  10458  fin23lem30  10459  fin56  10510  fin67  10512  hsmexlem9  10542  axcc4dom  10558  axdc3lem2  10568  axdc3lem4  10570  brdom3  10646  winainflem  10817  r1tskina  10906  indpi  11031  ltxrlt  11419  nn0sub  12696  nn0n0n1ge2b  12715  nn0ge2m1nn  12716  xnn0xr  12724  xnn0nemnf  12730  elnn0z  12746  nn0lt10b  12801  nn0le2is012  12803  nn0ind-raph  12839  uzin  13041  indstr2  13094  nn0ledivnn  13275  xrnemnf  13286  xrnepnf  13287  mnfltxr  13296  xnn0n0n1ge2b  13301  xnn0ge0  13303  xnn0xaddcl  13405  xnn0lenn0nn0  13415  xnn0xadd0  13417  xmullem2  13435  rexmul  13441  xnn0xrge0  13677  elfzonlteqm1  13916  elfznelfzo  13948  injresinjlem  13965  injresinj  13966  fldiv4p1lem1div2  14015  fldiv4lem1div2  14017  modfzo0difsn  14126  ssnn0fi  14168  fsuppmapnn0fiubex  14175  m1expcl2  14268  m1expeven  14292  zzlesq  14390  sq01  14410  expnngt1  14426  nn0opthi  14455  facp1  14463  faclbnd3  14477  faclbnd4lem1  14478  faclbnd4lem3  14480  bcn1  14498  hashnemnf  14529  hashv01gt1  14530  hashneq0  14549  hashrabrsn  14557  hashrabsn01  14558  hashrabsn1  14559  hashunx  14571  hashsnle1  14603  hashfzp1  14617  hash2pwpr  14662  hashge2el2difr  14667  swrdnd2  14847  pfxnd0  14880  repswswrd  14977  relexpsucl  15227  relexpsucr  15228  relexpcnv  15231  relexprelg  15234  relexpdmg  15238  relexprng  15242  relexpfld  15245  relexpaddg  15249  sumz  15932  arisum  16073  arisum2  16074  pwdif  16081  ntrivcvg  16110  prod1  16155  fprodfac  16184  mod2eq1n2dvds  16561  mulsucdiv2z  16567  nn0o1gt2  16595  nno  16596  nn0o  16597  sumeven  16601  sumodd  16602  divalglem1  16608  divalglem6  16612  gcdaddmlem  16740  dfgcd2  16763  mulgcd  16765  lcmf  16852  lcmfunsnlem2lem2  16858  lcmfunsnlem2  16859  prm2orodd  16910  dfphi2  16995  nnnn0modprm0  17028  prm23lt5  17036  oddprmdvds  17125  4sqlem19  17185  ramz  17247  prmolefac  17268  prmgaplem7  17279  cshwshashlem1  17317  ressval3d  17468  firest  17653  xpsfeq  17785  funcres2c  18128  ex-chn2  18862  smndex1basss  19154  smndex1mgm  19156  smndex1mndlem  19158  mulgnn0gsum  19340  symgfix2  19681  pmtrprfval  19752  m1expaddsub  19763  psgnprfval  19786  gsumpr  20220  gsumzunsnd  20221  0ringnnzr  20827  isfieldidl  21591  frgpcyg  21934  cnmsgnsubg  21938  psgninv  21943  zrhpsgnelbas  21955  m2detleiblem1  22994  symgmatr01lem  23023  indiscld  23464  pnfnei  23593  mnfnei  23594  alexsubALTlem2  24422  alexsubALTlem3  24423  dscmet  24946  xrtgioo  25181  ishl2  25746  iunmbl2  25933  icombl  25940  ioombl  25941  recnprss  26279  recnperf  26280  dvexp2  26329  dvexp3  26353  dvne0f1  26387  plypf1  26586  taylfvallem1  26741  taylfval  26743  tayl0  26746  coseq0negpitopi  26889  logfac  26986  cxpexp  27053  pythag  27202  reasinsin  27281  harmonicbnd3  27392  lgslem4  27684  gausslemma2dlem0i  27748  lgsquadlem2  27765  2lgslem3  27788  2lgs  27791  2lgsoddprmlem3  27798  2sqnn0  27822  2sqnn  27823  ltsres  28076  nolesgn2o  28085  nogesgn1o  28087  nosep1o  28095  nosep2o  28096  noetalem2  28156  sltsun1  28231  sltsun2  28232  eln0s  28804  n0zs  28832  bdaypw2n0bndlem  28906  bdaypw2n0bnd  28907  lfgrnloop  29760  uhgr2edg  29846  usgredg4  29855  usgredg2v  29865  usgrexmplef  29897  nb3grprlem1  30018  uvtx01vtx  30035  wlk1walk  30276  upgriswlk  30278  pthdadjvtx  30370  upgrwlkdvdelem  30379  pthdlem2lem  30410  pthspthcyc  30448  2pthon3v  30589  clwwlkn  30674  clwwlkneq0  30677  eupth2lem3lem4  30889  konigsberg  30915  3vfriswmgrlem  30935  1to2vfriswmgr  30937  1to3vfriswmgr  30938  frgrregorufr0  30982  numclwlk1  31029  ex-pr  31088  shunssi  32027  cvmdi  32983  1neg1t1neg1  33426  iundisj2cnt  33487  fz1nnct  33489  xrge0iifiso  34678  esumpr2  34810  measiuns  34961  sxbrsigalem0  35014  bnj964  35684  subfacval3  36162  kur14lem7  36185  satfrnmapom  36343  gonar  36368  goalr  36370  mrsubcv  36483  nepss  36698  nnuni  36707  fz0n  36711  bccolsum  36719  dfon2lem7  36766  altopthsn  36941  nn0prpw  37326  dissym1  37424  ordcmp  37450  ttciunun  37514  bj-currypeirce  37641  bj-jaoi1  37656  bj-jaoi2  37657  bj-ififc  37667  bj-andnotim  37673  bj-nfimexal  37723  bj-sbsb  37964  bj-elsn12g  38245  bj-ideqg1  38353  finxpreclem2  38581  wl-equsal1i  38744  tan2h  38803  poimirlem23  38829  poimirlem32  38838  itg2addnclem  38857  dfprop1  38913  orfa1  39285  orfa2  39286  inex3  39536  inxpex  39537  mopickr  39569  disjlem14  40099  elpadd0  41132  aks6d1c2p2  43435  quadfac  43521  sbor2  43531  sn-0ne2  43723  sn-0lt1  43805  hbtlem5  44395  omabs2  44595  safesnsupfiss  44677  safesnsupfidom1o  44679  safesnsupfilb  44680  rp-fakeimass  44774  rp-isfinite6  44780  pr2cv  44810  iunrelexp0  44963  relexpss1d  44966  relexpmulg  44971  iunrelexpmin2  44973  relexp01min  44974  relexp0a  44977  relexpxpmin  44978  relexpaddss  44979  clsk1indlem3  45304  ssrecnpr  45553  seff  45554  sblpnf  45555  expgrowthi  45578  dvconstbi  45579  19.33-2  45627  ax6e2ndeq  45802  en3lpVD  46087  undif3VD  46124  ax6e2ndeqVD  46151  ax6e2ndeqALT  46173  iooinlbub  46786  wrddun  48172  chndun  48177  chnrun  48182  elprneb  48372  euoreqb  48453  2reu3  48454  afvpcfv0  48489  afvfv0bi  48495  afvco2  48519  afv2orxorb  48571  afv2ndeffv0  48603  afv2fv0b  48609  fvmptrabdm  48636  nnmul2  48673  2ltceilhalf  48675  ceilhalfnn  48683  minusmodnep2tmod  48702  iccpartltu  48780  iccpartgtl  48781  iccpartgt  48782  iccpartleu  48783  iccpartgel  48784  iccpartnel  48793  elsprel  48830  prsprel  48842  sprsymrelfolem2  48848  paireqne  48866  odz2prm2pw  48921  fmtnofac1  48928  fmtno4prmfac  48930  31prm  48955  lighneallem2  48964  lighneallem3  48965  lighneallem4b  48967  lighneallem4  48968  ppivalnnnprm  48986  ppivalnn  48990  zeo2ALTV  49042  nn0o1gt2ALTV  49065  nn0oALTV  49067  stgoldbwt  49147  sbgoldbwt  49148  sbgoldbalt  49152  sbgoldbm  49155  sbgoldbo  49158  nnsum3primesle9  49165  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  wtgoldbnnsum4prm  49173  bgoldbnnsum3prm  49175  bgoldbtbndlem1  49176  bgoldbtbnd  49180  tgoldbach  49188  vopnbgrelself  49226  clnbgrgrim  49305  grtriproplem  49310  grtrif1o  49313  grtriclwlk3  49316  gpgedgvtx0  49432  gpgcubic  49450  gpg5nbgr3star  49452  gpgprismgr4cycllem3  49468  gpgprismgr4cycllem7  49472  gpgprismgr4cycllem10  49475  pgnbgreunbgrlem3  49489  pgnbgreunbgrlem6  49495  pgnbgreunbgr  49496  upgrwlkupwlk  49511  ztprmneprm  49790  islinindfis  49892  lindslinindsimp2lem5  49905  lindslinindsimp2  49906  lindsrng01  49911  elfzolborelfzop1  49962  flnn0div2ge  49976  blennn0elnn  50020  blen1b  50031  nnolog2flm1  50033  blengt1fldiv2p1  50036  0dig2pr01  50053  dignn0flhalf  50061  nn0sumshdiglemB  50063  nn0sumshdiglem1  50064  resum2sqorgt0  50152  rrx2plord2  50166  itsclc0yqsol  50207  mosssn  50257  mo0sn  50258  mofsssn  50288  mofmo  50289  f1omo  50338  f1omoOLD  50339  parhomcl2  51076