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  1884  19.33b  1885  nfim1  2199  dfsb2  2497  mooran1  2554  eueq3  3694  sbcor  3816  sspss  4077  sspsstr  4083  elun  4128  ssun  4170  inss  4223  raaan2  4496  ifbi  4523  ifcomnan  4557  rabsnifsb  4698  tpprceq3  4780  tppreqb  4781  pwpw0  4789  sssn  4802  snsssn  4817  preq12b  4826  prnebg  4832  preq12nebg  4839  elpr2elpr  4845  prproe  4881  3elpr2eq  4882  unissint  4948  zfpair  5391  propeqop  5482  propssopi  5483  opthhausdorff  5492  opthhausdorff0  5493  iunopeqop  5496  relsnb  5781  iresn0n0  6041  sotri2  6118  sotri3  6119  somincom  6123  ordssun  6456  unizlim  6477  onxpdisj  6480  tpres  7193  sorpssuni  7726  ordeleqon  7776  ordunisuc  7826  orduninsuc  7838  tfinds  7855  limomss  7866  limom  7877  soxp  8128  ressuppssdif  8184  tfr2b  8410  omopthi  8673  domnsym  9113  brwdom  9581  cantnfvalf  9679  ttrclselem1  9739  djuss  9934  djuunxp  9935  eldju2ndl  9938  eldju2ndr  9939  djuun  9940  updjud  9948  iscard3  10107  cflim2  10277  sornom  10291  isfin5  10313  isfin6  10314  sdom2en01  10316  fin23lem29  10355  fin23lem30  10356  fin56  10407  fin67  10409  hsmexlem9  10439  axcc4dom  10455  axdc3lem2  10465  axdc3lem4  10467  brdom3  10542  winainflem  10707  r1tskina  10796  indpi  10921  ltxrlt  11305  nn0sub  12551  nn0n0n1ge2b  12570  nn0ge2m1nn  12571  xnn0xr  12579  xnn0nemnf  12585  elnn0z  12601  nn0lt10b  12655  nn0le2is012  12657  nn0ind-raph  12693  uzin  12892  indstr2  12943  nn0ledivnn  13122  xrnemnf  13133  xrnepnf  13134  mnfltxr  13143  xnn0n0n1ge2b  13148  xnn0ge0  13150  xnn0xaddcl  13251  xnn0lenn0nn0  13261  xnn0xadd0  13263  xmullem2  13281  rexmul  13287  xnn0xrge0  13523  elfzonlteqm1  13757  elfznelfzo  13788  injresinjlem  13803  injresinj  13804  fldiv4p1lem1div2  13852  fldiv4lem1div2  13854  modfzo0difsn  13961  ssnn0fi  14003  fsuppmapnn0fiubex  14010  m1expcl2  14103  m1expeven  14127  zzlesq  14224  sq01  14243  expnngt1  14259  nn0opthi  14288  facp1  14296  faclbnd3  14310  faclbnd4lem1  14311  faclbnd4lem3  14313  bcn1  14331  hashnemnf  14362  hashv01gt1  14363  hashneq0  14382  hashrabrsn  14390  hashrabsn01  14391  hashrabsn1  14392  hashunx  14404  hashsnle1  14435  hashfzp1  14449  hash2pwpr  14494  hashge2el2difr  14499  swrdnd2  14673  pfxnd0  14706  repswswrd  14802  relexpsucl  15050  relexpsucr  15051  relexpcnv  15054  relexprelg  15057  relexpdmg  15061  relexprng  15065  relexpfld  15068  relexpaddg  15072  sumz  15738  arisum  15876  arisum2  15877  pwdif  15884  ntrivcvg  15913  prod1  15960  fprodfac  15989  mod2eq1n2dvds  16366  mulsucdiv2z  16372  nn0o1gt2  16400  nno  16401  nn0o  16402  sumeven  16406  sumodd  16407  divalglem1  16413  divalglem6  16417  gcdaddmlem  16543  dfgcd2  16565  mulgcd  16567  lcmf  16652  lcmfunsnlem2lem2  16658  lcmfunsnlem2  16659  prm2orodd  16710  dfphi2  16793  nnnn0modprm0  16826  prm23lt5  16834  oddprmdvds  16923  4sqlem19  16983  ramz  17045  prmolefac  17066  prmgaplem7  17077  cshwshashlem1  17115  ressval3d  17267  firest  17446  xpsfeq  17577  funcres2c  17916  smndex1basss  18883  smndex1mgm  18885  smndex1mndlem  18887  mulgnn0gsum  19063  symgfix2  19397  pmtrprfval  19468  m1expaddsub  19479  psgnprfval  19502  gsumpr  19936  gsumzunsnd  19937  0ringnnzr  20485  frgpcyg  21534  cnmsgnsubg  21537  psgninv  21542  zrhpsgnelbas  21554  m2detleiblem1  22562  symgmatr01lem  22591  indiscld  23029  pnfnei  23158  mnfnei  23159  alexsubALTlem2  23986  alexsubALTlem3  23987  dscmet  24511  xrtgioo  24746  ishl2  25322  iunmbl2  25510  icombl  25517  ioombl  25518  recnprss  25857  recnperf  25858  dvexp2  25910  dvexp3  25934  dvne0f1  25969  plypf1  26169  taylfvallem1  26316  taylfval  26318  tayl0  26321  coseq0negpitopi  26464  logfac  26562  cxpexp  26629  pythag  26779  reasinsin  26858  harmonicbnd3  26970  lgslem4  27263  gausslemma2dlem0i  27327  lgsquadlem2  27344  2lgslem3  27367  2lgs  27370  2lgsoddprmlem3  27377  2sqnn0  27401  2sqnn  27402  sltres  27626  nolesgn2o  27635  nogesgn1o  27637  nosep1o  27645  nosep2o  27646  noetalem2  27706  ssltun1  27772  ssltun2  27773  eln0s  28303  n0zs  28329  lfgrnloop  29104  uhgr2edg  29187  usgredg4  29196  usgredg2v  29206  usgrexmplef  29238  nb3grprlem1  29359  uvtx01vtx  29376  wlk1walk  29619  upgriswlk  29621  pthdadjvtx  29710  upgrwlkdvdelem  29718  pthdlem2lem  29749  pthspthcyc  29785  2pthon3v  29925  clwwlkn  30007  clwwlkneq0  30010  eupth2lem3lem4  30212  konigsberg  30238  3vfriswmgrlem  30258  1to2vfriswmgr  30260  1to3vfriswmgr  30261  frgrregorufr0  30305  numclwlk1  30352  ex-pr  30411  shunssi  31349  cvmdi  32305  1neg1t1neg1  32715  iundisj2cnt  32776  fz1nnct  32780  xrge0iifiso  33966  esumpr2  34098  measiuns  34248  sxbrsigalem0  34303  bnj964  34974  subfacval3  35211  kur14lem7  35234  satfrnmapom  35392  gonar  35417  goalr  35419  mrsubcv  35532  nepss  35735  nnuni  35744  fz0n  35748  bccolsum  35756  dfon2lem7  35807  altopthsn  35979  elhf2  36193  nn0prpw  36341  dissym1  36439  ordcmp  36465  bj-currypeirce  36575  bj-jaoi1  36589  bj-jaoi2  36590  bj-ififc  36600  bj-andnotim  36606  bj-nfimexal  36644  bj-sbsb  36855  bj-elsn12g  37078  bj-ideqg1  37182  finxpreclem2  37408  wl-equsal1i  37562  tan2h  37636  poimirlem23  37667  poimirlem32  37676  itg2addnclem  37695  orfa1  38109  orfa2  38110  imaexALTV  38348  inex3  38356  inxpex  38357  mopickr  38381  disjlem14  38816  elpadd0  39828  aks6d1c2p2  42132  sbor2  42263  sn-0ne2  42449  sn-0lt1  42506  hbtlem5  43152  omabs2  43356  safesnsupfiss  43439  safesnsupfidom1o  43441  safesnsupfilb  43442  rp-fakeimass  43536  rp-isfinite6  43542  pr2cv  43572  iunrelexp0  43726  relexpss1d  43729  relexpmulg  43734  iunrelexpmin2  43736  relexp01min  43737  relexp0a  43740  relexpxpmin  43741  relexpaddss  43742  clsk1indlem3  44067  ssrecnpr  44332  seff  44333  sblpnf  44334  expgrowthi  44357  dvconstbi  44358  19.33-2  44406  ax6e2ndeq  44584  en3lpVD  44869  undif3VD  44906  ax6e2ndeqVD  44933  ax6e2ndeqALT  44955  iooinlbub  45530  elprneb  47058  euoreqb  47138  2reu3  47139  afvpcfv0  47175  afvfv0bi  47181  afvco2  47205  afv2orxorb  47257  afv2ndeffv0  47289  afv2fv0b  47295  fvmptrabdm  47322  2ltceilhalf  47357  ceilhalfnn  47365  minusmodnep2tmod  47382  iccpartltu  47439  iccpartgtl  47440  iccpartgt  47441  iccpartleu  47442  iccpartgel  47443  iccpartnel  47452  elsprel  47489  prsprel  47501  sprsymrelfolem2  47507  paireqne  47525  odz2prm2pw  47577  fmtnofac1  47584  fmtno4prmfac  47586  31prm  47611  lighneallem2  47620  lighneallem3  47621  lighneallem4b  47623  lighneallem4  47624  zeo2ALTV  47685  nn0o1gt2ALTV  47708  nn0oALTV  47710  stgoldbwt  47790  sbgoldbwt  47791  sbgoldbalt  47795  sbgoldbm  47798  sbgoldbo  47801  nnsum3primesle9  47808  nnsum4primeseven  47814  nnsum4primesevenALTV  47815  wtgoldbnnsum4prm  47816  bgoldbnnsum3prm  47818  bgoldbtbndlem1  47819  bgoldbtbnd  47823  tgoldbach  47831  vopnbgrelself  47868  clnbgrgrim  47947  grtriproplem  47951  grtrif1o  47954  grtriclwlk3  47957  gpgedgvtx0  48065  gpgcubic  48081  gpg5nbgr3star  48083  gpgprismgr4cycllem3  48096  gpgprismgr4cycllem7  48100  gpgprismgr4cycllem10  48103  upgrwlkupwlk  48115  ztprmneprm  48322  islinindfis  48425  lindslinindsimp2lem5  48438  lindslinindsimp2  48439  lindsrng01  48444  elfzolborelfzop1  48495  flnn0div2ge  48513  blennn0elnn  48557  blen1b  48568  nnolog2flm1  48570  blengt1fldiv2p1  48573  0dig2pr01  48590  dignn0flhalf  48598  nn0sumshdiglemB  48600  nn0sumshdiglem1  48601  resum2sqorgt0  48689  rrx2xpref1o  48698  rrx2plord2  48702  itsclc0yqsol  48744  mosssn  48793  mo0sn  48794  mofsssn  48824  mofmo  48825  f1omo  48868