Theorem jaoi 857

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 851	. . 3 ⊢ ((𝜑 ∨ 𝜒) → (¬ 𝜑 → 𝜒))
2		jaoi.2	. . 3 ⊢ (𝜒 → 𝜓)
3	1, 2	syl6 35	. 2 ⊢ ((𝜑 ∨ 𝜒) → (¬ 𝜑 → 𝜓))
4		jaoi.1	. 2 ⊢ (𝜑 → 𝜓)
5	3, 4	pm2.61d2 181	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:  jao1i  858  jaod  859  pm1.4  869  pm3.2ni  880  pm1.2  903  pm2.4  906  pm2.41  907  orim12i  908  pm1.5  919  pm2.42  944  jaoa  957  jaoian  958  pm4.44  998  andi  1009  ecase3  1032  cases2ALT  1048  consensus  1052  jaoi3  1060  1fpid3  1081  19.33  1885  19.33b  1886  nfim1  2206  dfsb2  2497  mooran1  2555  eueq3  3669  sbcor  3791  sspss  4054  sspsstr  4060  elun  4105  ssun  4147  inss  4200  raaan2  4475  ifbi  4502  ifcomnan  4536  rabsnifsb  4679  tpprceq3  4760  tppreqb  4761  pwpw0  4769  sssn  4782  snsssn  4797  preq12b  4806  prnebg  4812  preq12nebg  4819  elpr2elpr  4825  prproe  4861  3elpr2eq  4862  unissint  4927  zfpair  5366  propeqop  5455  propssopi  5456  opthhausdorff  5465  opthhausdorff0  5466  iunopeqop  5469  relsnb  5751  iresn0n0  6013  sotri2  6086  sotri3  6087  somincom  6091  ordssun  6421  unizlim  6441  onxpdisj  6444  tpres  7147  sorpssuni  7677  ordeleqon  7727  ordunisuc  7774  orduninsuc  7785  tfinds  7802  limomss  7813  limom  7824  soxp  8071  ressuppssdif  8127  tfr2b  8327  omopthi  8589  domnsym  9031  ordfin  9140  brwdom  9472  cantnfvalf  9574  ttrclselem1  9634  djuss  9832  djuunxp  9833  eldju2ndl  9836  eldju2ndr  9837  djuun  9838  updjud  9846  iscard3  10003  cflim2  10173  sornom  10187  isfin5  10209  isfin6  10210  sdom2en01  10212  fin23lem29  10251  fin23lem30  10252  fin56  10303  fin67  10305  hsmexlem9  10335  axcc4dom  10351  axdc3lem2  10361  axdc3lem4  10363  brdom3  10438  winainflem  10604  r1tskina  10693  indpi  10818  ltxrlt  11203  nn0sub  12451  nn0n0n1ge2b  12470  nn0ge2m1nn  12471  xnn0xr  12479  xnn0nemnf  12485  elnn0z  12501  nn0lt10b  12554  nn0le2is012  12556  nn0ind-raph  12592  uzin  12787  indstr2  12840  nn0ledivnn  13020  xrnemnf  13031  xrnepnf  13032  mnfltxr  13041  xnn0n0n1ge2b  13046  xnn0ge0  13048  xnn0xaddcl  13150  xnn0lenn0nn0  13160  xnn0xadd0  13162  xmullem2  13180  rexmul  13186  xnn0xrge0  13422  elfzonlteqm1  13657  elfznelfzo  13689  injresinjlem  13706  injresinj  13707  fldiv4p1lem1div2  13755  fldiv4lem1div2  13757  modfzo0difsn  13866  ssnn0fi  13908  fsuppmapnn0fiubex  13915  m1expcl2  14008  m1expeven  14032  zzlesq  14129  sq01  14148  expnngt1  14164  nn0opthi  14193  facp1  14201  faclbnd3  14215  faclbnd4lem1  14216  faclbnd4lem3  14218  bcn1  14236  hashnemnf  14267  hashv01gt1  14268  hashneq0  14287  hashrabrsn  14295  hashrabsn01  14296  hashrabsn1  14297  hashunx  14309  hashsnle1  14340  hashfzp1  14354  hash2pwpr  14399  hashge2el2difr  14404  swrdnd2  14579  pfxnd0  14612  repswswrd  14707  relexpsucl  14954  relexpsucr  14955  relexpcnv  14958  relexprelg  14961  relexpdmg  14965  relexprng  14969  relexpfld  14972  relexpaddg  14976  sumz  15645  arisum  15783  arisum2  15784  pwdif  15791  ntrivcvg  15820  prod1  15867  fprodfac  15896  mod2eq1n2dvds  16274  mulsucdiv2z  16280  nn0o1gt2  16308  nno  16309  nn0o  16310  sumeven  16314  sumodd  16315  divalglem1  16321  divalglem6  16325  gcdaddmlem  16451  dfgcd2  16473  mulgcd  16475  lcmf  16560  lcmfunsnlem2lem2  16566  lcmfunsnlem2  16567  prm2orodd  16618  dfphi2  16701  nnnn0modprm0  16734  prm23lt5  16742  oddprmdvds  16831  4sqlem19  16891  ramz  16953  prmolefac  16974  prmgaplem7  16985  cshwshashlem1  17023  ressval3d  17173  firest  17352  xpsfeq  17484  funcres2c  17827  ex-chn2  18561  smndex1basss  18830  smndex1mgm  18832  smndex1mndlem  18834  mulgnn0gsum  19010  symgfix2  19345  pmtrprfval  19416  m1expaddsub  19427  psgnprfval  19450  gsumpr  19884  gsumzunsnd  19885  0ringnnzr  20458  frgpcyg  21528  cnmsgnsubg  21532  psgninv  21537  zrhpsgnelbas  21549  m2detleiblem1  22568  symgmatr01lem  22597  indiscld  23035  pnfnei  23164  mnfnei  23165  alexsubALTlem2  23992  alexsubALTlem3  23993  dscmet  24516  xrtgioo  24751  ishl2  25326  iunmbl2  25514  icombl  25521  ioombl  25522  recnprss  25861  recnperf  25862  dvexp2  25914  dvexp3  25938  dvne0f1  25973  plypf1  26173  taylfvallem1  26320  taylfval  26322  tayl0  26325  coseq0negpitopi  26468  logfac  26566  cxpexp  26633  pythag  26783  reasinsin  26862  harmonicbnd3  26974  lgslem4  27267  gausslemma2dlem0i  27331  lgsquadlem2  27348  2lgslem3  27371  2lgs  27374  2lgsoddprmlem3  27381  2sqnn0  27405  2sqnn  27406  ltsres  27630  nolesgn2o  27639  nogesgn1o  27641  nosep1o  27649  nosep2o  27650  noetalem2  27710  sltsun1  27784  sltsun2  27785  eln0s  28357  n0zs  28385  bdaypw2n0bndlem  28459  bdaypw2n0bnd  28460  lfgrnloop  29198  uhgr2edg  29281  usgredg4  29290  usgredg2v  29300  usgrexmplef  29332  nb3grprlem1  29453  uvtx01vtx  29470  wlk1walk  29712  upgriswlk  29714  pthdadjvtx  29801  upgrwlkdvdelem  29809  pthdlem2lem  29840  pthspthcyc  29876  2pthon3v  30016  clwwlkn  30101  clwwlkneq0  30104  eupth2lem3lem4  30306  konigsberg  30332  3vfriswmgrlem  30352  1to2vfriswmgr  30354  1to3vfriswmgr  30355  frgrregorufr0  30399  numclwlk1  30446  ex-pr  30505  shunssi  31443  cvmdi  32399  1neg1t1neg1  32817  iundisj2cnt  32879  fz1nnct  32881  xrge0iifiso  34092  esumpr2  34224  measiuns  34374  sxbrsigalem0  34428  bnj964  35099  subfacval3  35383  kur14lem7  35406  satfrnmapom  35564  gonar  35589  goalr  35591  mrsubcv  35704  nepss  35912  nnuni  35921  fz0n  35925  bccolsum  35933  dfon2lem7  35981  altopthsn  36155  elhf2  36369  nn0prpw  36517  dissym1  36615  ordcmp  36641  bj-currypeirce  36757  bj-jaoi1  36771  bj-jaoi2  36772  bj-ififc  36782  bj-andnotim  36788  bj-nfimexal  36826  bj-sbsb  37038  bj-elsn12g  37261  bj-ideqg1  37369  finxpreclem2  37595  wl-equsal1i  37749  tan2h  37813  poimirlem23  37844  poimirlem32  37853  itg2addnclem  37872  orfa1  38286  orfa2  38287  inex3  38531  inxpex  38532  mopickr  38556  disjlem14  39057  elpadd0  40069  aks6d1c2p2  42373  sbor2  42466  sn-0ne2  42661  sn-0lt1  42730  hbtlem5  43370  omabs2  43574  safesnsupfiss  43656  safesnsupfidom1o  43658  safesnsupfilb  43659  rp-fakeimass  43753  rp-isfinite6  43759  pr2cv  43789  iunrelexp0  43943  relexpss1d  43946  relexpmulg  43951  iunrelexpmin2  43953  relexp01min  43954  relexp0a  43957  relexpxpmin  43958  relexpaddss  43959  clsk1indlem3  44284  ssrecnpr  44549  seff  44550  sblpnf  44551  expgrowthi  44574  dvconstbi  44575  19.33-2  44623  ax6e2ndeq  44800  en3lpVD  45085  undif3VD  45122  ax6e2ndeqVD  45149  ax6e2ndeqALT  45171  iooinlbub  45747  elprneb  47275  euoreqb  47355  2reu3  47356  afvpcfv0  47392  afvfv0bi  47398  afvco2  47422  afv2orxorb  47474  afv2ndeffv0  47506  afv2fv0b  47512  fvmptrabdm  47539  2ltceilhalf  47574  ceilhalfnn  47582  minusmodnep2tmod  47599  iccpartltu  47671  iccpartgtl  47672  iccpartgt  47673  iccpartleu  47674  iccpartgel  47675  iccpartnel  47684  elsprel  47721  prsprel  47733  sprsymrelfolem2  47739  paireqne  47757  odz2prm2pw  47809  fmtnofac1  47816  fmtno4prmfac  47818  31prm  47843  lighneallem2  47852  lighneallem3  47853  lighneallem4b  47855  lighneallem4  47856  zeo2ALTV  47917  nn0o1gt2ALTV  47940  nn0oALTV  47942  stgoldbwt  48022  sbgoldbwt  48023  sbgoldbalt  48027  sbgoldbm  48030  sbgoldbo  48033  nnsum3primesle9  48040  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  wtgoldbnnsum4prm  48048  bgoldbnnsum3prm  48050  bgoldbtbndlem1  48051  bgoldbtbnd  48055  tgoldbach  48063  vopnbgrelself  48101  clnbgrgrim  48180  grtriproplem  48185  grtrif1o  48188  grtriclwlk3  48191  gpgedgvtx0  48307  gpgcubic  48325  gpg5nbgr3star  48327  gpgprismgr4cycllem3  48343  gpgprismgr4cycllem7  48347  gpgprismgr4cycllem10  48350  pgnbgreunbgrlem3  48364  pgnbgreunbgrlem6  48370  pgnbgreunbgr  48371  upgrwlkupwlk  48386  ztprmneprm  48593  islinindfis  48695  lindslinindsimp2lem5  48708  lindslinindsimp2  48709  lindsrng01  48714  elfzolborelfzop1  48765  flnn0div2ge  48779  blennn0elnn  48823  blen1b  48834  nnolog2flm1  48836  blengt1fldiv2p1  48839  0dig2pr01  48856  dignn0flhalf  48864  nn0sumshdiglemB  48866  nn0sumshdiglem1  48867  resum2sqorgt0  48955  rrx2xpref1o  48964  rrx2plord2  48968  itsclc0yqsol  49010  mosssn  49060  mo0sn  49061  mofsssn  49091  mofmo  49092  f1omo  49138  f1omoOLD  49139