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  1917  19.33b  1918  nfim1  2235  dfsb2  2522  mooran1  2580  eueq3  3669  sbcor  3789  sspss  4050  sspsstr  4057  elun  4100  ssun  4141  inss  4194  raaan2  4478  ifbi  4505  ifcomnan  4539  rabsnifsb  4683  tpprceq3  4767  tppreqb  4768  pwpw0  4774  sssn  4787  snsssn  4801  preq12b  4810  prnebg  4816  preq12nebg  4823  elpr2elpr  4829  prproe  4865  3elpr2eq  4866  unissint  4932  zfpair  5386  axprg  5402  propeqop  5484  propssopi  5485  opthhausdorff  5494  opthhausdorff0  5495  iunopeqop  5498  iunopeqopOLD  5499  relsnb  5783  iresn0n0  6050  sotri2  6123  sotri3  6124  somincom  6128  ordssun  6462  unizlim  6482  onxpdisj  6485  tpres  7200  sorpssuni  7733  ordeleqon  7781  ordunisuc  7828  orduninsuc  7839  tfinds  7856  limomss  7867  limom  7878  soxp  8127  ressuppssdif  8183  tfr2b  8385  omopthi  8649  domnsym  9101  ordfin  9210  brwdom  9539  cantnfvalf  9644  ttrclselem1  9704  djuss  9925  djuunxp  9926  eldju2ndl  9929  eldju2ndr  9930  djuun  9931  updjud  9939  iscard3  10096  cflim2  10265  sornom  10279  isfin5  10301  isfin6  10302  sdom2en01  10304  fin23lem29  10343  fin23lem30  10344  fin56  10395  fin67  10397  hsmexlem9  10427  axcc4dom  10443  axdc3lem2  10453  axdc3lem4  10455  brdom3  10531  winainflem  10702  r1tskina  10791  indpi  10916  ltxrlt  11304  nn0sub  12578  nn0n0n1ge2b  12597  nn0ge2m1nn  12598  xnn0xr  12606  xnn0nemnf  12612  elnn0z  12628  nn0lt10b  12683  nn0le2is012  12685  nn0ind-raph  12721  uzin  12923  indstr2  12976  nn0ledivnn  13157  xrnemnf  13168  xrnepnf  13169  mnfltxr  13178  xnn0n0n1ge2b  13183  xnn0ge0  13185  xnn0xaddcl  13287  xnn0lenn0nn0  13297  xnn0xadd0  13299  xmullem2  13317  rexmul  13323  xnn0xrge0  13559  elfzonlteqm1  13797  elfznelfzo  13829  injresinjlem  13846  injresinj  13847  fldiv4p1lem1div2  13896  fldiv4lem1div2  13898  modfzo0difsn  14007  ssnn0fi  14049  fsuppmapnn0fiubex  14056  m1expcl2  14149  m1expeven  14173  zzlesq  14270  sq01  14289  expnngt1  14305  nn0opthi  14334  facp1  14342  faclbnd3  14356  faclbnd4lem1  14357  faclbnd4lem3  14359  bcn1  14377  hashnemnf  14408  hashv01gt1  14409  hashneq0  14428  hashrabrsn  14436  hashrabsn01  14437  hashrabsn1  14438  hashunx  14450  hashsnle1  14482  hashfzp1  14496  hash2pwpr  14541  hashge2el2difr  14546  swrdnd2  14725  pfxnd0  14758  repswswrd  14855  relexpsucl  15104  relexpsucr  15105  relexpcnv  15108  relexprelg  15111  relexpdmg  15115  relexprng  15119  relexpfld  15122  relexpaddg  15126  sumz  15808  arisum  15949  arisum2  15950  pwdif  15957  ntrivcvg  15986  prod1  16031  fprodfac  16060  mod2eq1n2dvds  16437  mulsucdiv2z  16443  nn0o1gt2  16471  nno  16472  nn0o  16473  sumeven  16477  sumodd  16478  divalglem1  16484  divalglem6  16488  gcdaddmlem  16614  dfgcd2  16636  mulgcd  16638  lcmf  16723  lcmfunsnlem2lem2  16729  lcmfunsnlem2  16730  prm2orodd  16781  dfphi2  16865  nnnn0modprm0  16898  prm23lt5  16906  oddprmdvds  16995  4sqlem19  17055  ramz  17117  prmolefac  17138  prmgaplem7  17149  cshwshashlem1  17187  ressval3d  17338  firest  17517  xpsfeq  17649  funcres2c  17992  ex-chn2  18726  smndex1basss  19017  smndex1mgm  19019  smndex1mndlem  19021  mulgnn0gsum  19203  symgfix2  19543  pmtrprfval  19614  m1expaddsub  19625  psgnprfval  19648  gsumpr  20082  gsumzunsnd  20083  0ringnnzr  20686  isfieldidl  21449  frgpcyg  21786  cnmsgnsubg  21790  psgninv  21795  zrhpsgnelbas  21807  m2detleiblem1  22846  symgmatr01lem  22875  indiscld  23316  pnfnei  23445  mnfnei  23446  alexsubALTlem2  24274  alexsubALTlem3  24275  dscmet  24798  xrtgioo  25033  ishl2  25598  iunmbl2  25785  icombl  25792  ioombl  25793  recnprss  26131  recnperf  26132  dvexp2  26181  dvexp3  26205  dvne0f1  26239  plypf1  26438  taylfvallem1  26593  taylfval  26595  tayl0  26598  coseq0negpitopi  26741  logfac  26838  cxpexp  26905  pythag  27054  reasinsin  27133  harmonicbnd3  27244  lgslem4  27536  gausslemma2dlem0i  27600  lgsquadlem2  27617  2lgslem3  27640  2lgs  27643  2lgsoddprmlem3  27650  2sqnn0  27674  2sqnn  27675  ltsres  27898  nolesgn2o  27907  nogesgn1o  27909  nosep1o  27917  nosep2o  27918  noetalem2  27978  sltsun1  28053  sltsun2  28054  eln0s  28626  n0zs  28654  bdaypw2n0bndlem  28728  bdaypw2n0bnd  28729  lfgrnloop  29582  uhgr2edg  29668  usgredg4  29677  usgredg2v  29687  usgrexmplef  29719  nb3grprlem1  29840  uvtx01vtx  29857  wlk1walk  30098  upgriswlk  30100  pthdadjvtx  30192  upgrwlkdvdelem  30201  pthdlem2lem  30232  pthspthcyc  30270  2pthon3v  30411  clwwlkn  30496  clwwlkneq0  30499  eupth2lem3lem4  30711  konigsberg  30737  3vfriswmgrlem  30757  1to2vfriswmgr  30759  1to3vfriswmgr  30760  frgrregorufr0  30804  numclwlk1  30851  ex-pr  30910  shunssi  31849  cvmdi  32805  1neg1t1neg1  33209  iundisj2cnt  33270  fz1nnct  33272  xrge0iifiso  34445  esumpr2  34577  measiuns  34728  sxbrsigalem0  34782  bnj964  35452  subfacval3  35768  kur14lem7  35791  satfrnmapom  35949  gonar  35974  goalr  35976  mrsubcv  36089  nepss  36297  nnuni  36306  fz0n  36310  bccolsum  36318  dfon2lem7  36366  altopthsn  36541  elhf2  36755  nn0prpw  36942  dissym1  37040  ordcmp  37066  ttciunun  37130  bj-currypeirce  37257  bj-jaoi1  37272  bj-jaoi2  37273  bj-ififc  37283  bj-andnotim  37289  bj-nfimexal  37339  bj-sbsb  37580  bj-elsn12g  37804  bj-ideqg1  37916  finxpreclem2  38144  wl-equsal1i  38307  tan2h  38366  poimirlem23  38392  poimirlem32  38401  itg2addnclem  38420  orfa1  38835  orfa2  38836  inex3  39086  inxpex  39087  mopickr  39119  disjlem14  39649  elpadd0  40682  aks6d1c2p2  42985  quadfac  43071  sbor2  43080  sn-0ne2  43281  sn-0lt1  43363  hbtlem5  43969  omabs2  44173  safesnsupfiss  44255  safesnsupfidom1o  44257  safesnsupfilb  44258  rp-fakeimass  44352  rp-isfinite6  44358  pr2cv  44388  iunrelexp0  44542  relexpss1d  44545  relexpmulg  44550  iunrelexpmin2  44552  relexp01min  44553  relexp0a  44556  relexpxpmin  44557  relexpaddss  44558  clsk1indlem3  44883  ssrecnpr  45132  seff  45133  sblpnf  45134  expgrowthi  45157  dvconstbi  45158  19.33-2  45206  ax6e2ndeq  45382  en3lpVD  45667  undif3VD  45704  ax6e2ndeqVD  45731  ax6e2ndeqALT  45753  iooinlbub  46331  wrddun  47717  chndun  47722  chnrun  47727  elprneb  47917  euoreqb  47997  2reu3  47998  afvpcfv0  48034  afvfv0bi  48040  afvco2  48064  afv2orxorb  48116  afv2ndeffv0  48148  afv2fv0b  48154  fvmptrabdm  48181  nnmul2  48218  2ltceilhalf  48220  ceilhalfnn  48228  minusmodnep2tmod  48247  iccpartltu  48325  iccpartgtl  48326  iccpartgt  48327  iccpartleu  48328  iccpartgel  48329  iccpartnel  48338  elsprel  48375  prsprel  48387  sprsymrelfolem2  48393  paireqne  48411  odz2prm2pw  48466  fmtnofac1  48473  fmtno4prmfac  48475  31prm  48500  lighneallem2  48509  lighneallem3  48510  lighneallem4b  48512  lighneallem4  48513  ppivalnnnprm  48531  ppivalnn  48535  zeo2ALTV  48587  nn0o1gt2ALTV  48610  nn0oALTV  48612  stgoldbwt  48692  sbgoldbwt  48693  sbgoldbalt  48697  sbgoldbm  48700  sbgoldbo  48703  nnsum3primesle9  48710  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  wtgoldbnnsum4prm  48718  bgoldbnnsum3prm  48720  bgoldbtbndlem1  48721  bgoldbtbnd  48725  tgoldbach  48733  vopnbgrelself  48771  clnbgrgrim  48850  grtriproplem  48855  grtrif1o  48858  grtriclwlk3  48861  gpgedgvtx0  48977  gpgcubic  48995  gpg5nbgr3star  48997  gpgprismgr4cycllem3  49013  gpgprismgr4cycllem7  49017  gpgprismgr4cycllem10  49020  pgnbgreunbgrlem3  49034  pgnbgreunbgrlem6  49040  pgnbgreunbgr  49041  upgrwlkupwlk  49056  ztprmneprm  49277  islinindfis  49379  lindslinindsimp2lem5  49392  lindslinindsimp2  49393  lindsrng01  49398  elfzolborelfzop1  49449  flnn0div2ge  49463  blennn0elnn  49507  blen1b  49518  nnolog2flm1  49520  blengt1fldiv2p1  49523  0dig2pr01  49540  dignn0flhalf  49548  nn0sumshdiglemB  49550  nn0sumshdiglem1  49551  resum2sqorgt0  49639  rrx2xpref1o  49648  rrx2plord2  49652  itsclc0yqsol  49694  mosssn  49743  mo0sn  49744  mofsssn  49774  mofmo  49775  f1omo  49819  f1omoOLD  49820