Theorem jaoi 858

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 852	. . 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 848

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 849

This theorem is referenced by:  jao1i  859  jaod  860  pm1.4  870  pm3.2ni  881  pm1.2  904  pm2.4  907  pm2.41  908  orim12i  909  pm1.5  920  pm2.42  945  jaoa  958  jaoian  959  pm4.44  999  andi  1010  ecase3  1033  cases2ALT  1049  consensus  1053  jaoi3  1061  1fpid3  1082  19.33  1884  19.33b  1885  nfim1  2199  dfsb2  2498  mooran1  2555  eueq3  3717  sbcor  3839  sspss  4102  sspsstr  4108  elun  4153  ssun  4195  inss  4248  raaan2  4521  ifbi  4548  ifcomnan  4582  rabsnifsb  4722  tpprceq3  4804  tppreqb  4805  pwpw0  4813  sssn  4826  snsssn  4841  preq12b  4850  prnebg  4856  preq12nebg  4863  elpr2elpr  4869  prproe  4905  3elpr2eq  4906  unissint  4972  zfpair  5421  propeqop  5512  propssopi  5513  opthhausdorff  5522  opthhausdorff0  5523  iunopeqop  5526  relsnb  5812  iresn0n0  6072  sotri2  6149  sotri3  6150  somincom  6154  ordssun  6486  unizlim  6507  onxpdisj  6510  tpres  7221  sorpssuni  7752  ordeleqon  7802  ordunisuc  7852  orduninsuc  7864  tfinds  7881  limomss  7892  limom  7903  soxp  8154  ressuppssdif  8210  tfr2b  8436  omopthi  8699  domnsym  9139  brwdom  9607  cantnfvalf  9705  ttrclselem1  9765  djuss  9960  djuunxp  9961  eldju2ndl  9964  eldju2ndr  9965  djuun  9966  updjud  9974  iscard3  10133  cflim2  10303  sornom  10317  isfin5  10339  isfin6  10340  sdom2en01  10342  fin23lem29  10381  fin23lem30  10382  fin56  10433  fin67  10435  hsmexlem9  10465  axcc4dom  10481  axdc3lem2  10491  axdc3lem4  10493  brdom3  10568  winainflem  10733  r1tskina  10822  indpi  10947  ltxrlt  11331  nn0sub  12576  nn0n0n1ge2b  12595  nn0ge2m1nn  12596  xnn0xr  12604  xnn0nemnf  12610  elnn0z  12626  nn0lt10b  12680  nn0le2is012  12682  nn0ind-raph  12718  uzin  12918  indstr2  12969  nn0ledivnn  13148  xrnemnf  13159  xrnepnf  13160  mnfltxr  13169  xnn0n0n1ge2b  13174  xnn0ge0  13176  xnn0xaddcl  13277  xnn0lenn0nn0  13287  xnn0xadd0  13289  xmullem2  13307  rexmul  13313  xnn0xrge0  13546  elfzonlteqm1  13780  elfznelfzo  13811  injresinjlem  13826  injresinj  13827  fldiv4p1lem1div2  13875  fldiv4lem1div2  13877  modfzo0difsn  13984  ssnn0fi  14026  fsuppmapnn0fiubex  14033  m1expcl2  14126  m1expeven  14150  zzlesq  14245  sq01  14264  expnngt1  14280  nn0opthi  14309  facp1  14317  faclbnd3  14331  faclbnd4lem1  14332  faclbnd4lem3  14334  bcn1  14352  hashnemnf  14383  hashv01gt1  14384  hashneq0  14403  hashrabrsn  14411  hashrabsn01  14412  hashrabsn1  14413  hashunx  14425  hashsnle1  14456  hashfzp1  14470  hash2pwpr  14515  hashge2el2difr  14520  swrdnd2  14693  pfxnd0  14726  repswswrd  14822  relexpsucl  15070  relexpsucr  15071  relexpcnv  15074  relexprelg  15077  relexpdmg  15081  relexprng  15085  relexpfld  15088  relexpaddg  15092  sumz  15758  arisum  15896  arisum2  15897  pwdif  15904  ntrivcvg  15933  prod1  15980  fprodfac  16009  mod2eq1n2dvds  16384  mulsucdiv2z  16390  nn0o1gt2  16418  nno  16419  nn0o  16420  sumeven  16424  sumodd  16425  divalglem1  16431  divalglem6  16435  gcdaddmlem  16561  dfgcd2  16583  mulgcd  16585  lcmf  16670  lcmfunsnlem2lem2  16676  lcmfunsnlem2  16677  prm2orodd  16728  dfphi2  16811  nnnn0modprm0  16844  prm23lt5  16852  oddprmdvds  16941  4sqlem19  17001  ramz  17063  prmolefac  17084  prmgaplem7  17095  cshwshashlem1  17133  ressval3d  17292  firest  17477  xpsfeq  17608  funcres2c  17948  smndex1basss  18918  smndex1mgm  18920  smndex1mndlem  18922  mulgnn0gsum  19098  symgfix2  19434  pmtrprfval  19505  m1expaddsub  19516  psgnprfval  19539  gsumpr  19973  gsumzunsnd  19974  0ringnnzr  20525  sralemOLD  21176  frgpcyg  21592  cnmsgnsubg  21595  psgninv  21600  zrhpsgnelbas  21612  m2detleiblem1  22630  symgmatr01lem  22659  indiscld  23099  pnfnei  23228  mnfnei  23229  alexsubALTlem2  24056  alexsubALTlem3  24057  dscmet  24585  xrtgioo  24828  ishl2  25404  iunmbl2  25592  icombl  25599  ioombl  25600  recnprss  25939  recnperf  25940  dvexp2  25992  dvexp3  26016  dvne0f1  26051  plypf1  26251  taylfvallem1  26398  taylfval  26400  tayl0  26403  coseq0negpitopi  26545  logfac  26643  cxpexp  26710  pythag  26860  reasinsin  26939  harmonicbnd3  27051  lgslem4  27344  gausslemma2dlem0i  27408  lgsquadlem2  27425  2lgslem3  27448  2lgs  27451  2lgsoddprmlem3  27458  2sqnn0  27482  2sqnn  27483  sltres  27707  nolesgn2o  27716  nogesgn1o  27718  nosep1o  27726  nosep2o  27727  noetalem2  27787  ssltun1  27853  ssltun2  27854  eln0s  28358  n0zs  28375  cchhllemOLD  28902  lfgrnloop  29142  uhgr2edg  29225  usgredg4  29234  usgredg2v  29244  usgrexmplef  29276  nb3grprlem1  29397  uvtx01vtx  29414  wlk1walk  29657  upgriswlk  29659  pthdadjvtx  29748  upgrwlkdvdelem  29756  pthdlem2lem  29787  pthspthcyc  29823  2pthon3v  29963  clwwlkn  30045  clwwlkneq0  30048  eupth2lem3lem4  30250  konigsberg  30276  3vfriswmgrlem  30296  1to2vfriswmgr  30298  1to3vfriswmgr  30299  frgrregorufr0  30343  numclwlk1  30390  ex-pr  30449  shunssi  31387  cvmdi  32343  1neg1t1neg1  32748  iundisj2cnt  32801  fz1nnct  32805  xrge0iifiso  33934  esumpr2  34068  measiuns  34218  sxbrsigalem0  34273  bnj964  34957  subfacval3  35194  kur14lem7  35217  satfrnmapom  35375  gonar  35400  goalr  35402  mrsubcv  35515  nepss  35718  nnuni  35727  fz0n  35731  bccolsum  35739  dfon2lem7  35790  altopthsn  35962  elhf2  36176  nn0prpw  36324  dissym1  36422  ordcmp  36448  bj-currypeirce  36558  bj-jaoi1  36572  bj-jaoi2  36573  bj-ififc  36583  bj-andnotim  36589  bj-nfimexal  36627  bj-sbsb  36838  bj-elsn12g  37061  bj-ideqg1  37165  finxpreclem2  37391  wl-equsal1i  37545  tan2h  37619  poimirlem23  37650  poimirlem32  37659  itg2addnclem  37678  orfa1  38092  orfa2  38093  imaexALTV  38331  inex3  38339  inxpex  38340  mopickr  38364  disjlem14  38799  elpadd0  39811  aks6d1c2p2  42120  sbor2  42251  sn-0ne2  42436  sn-0lt1  42493  hbtlem5  43140  omabs2  43345  safesnsupfiss  43428  safesnsupfidom1o  43430  safesnsupfilb  43431  rp-fakeimass  43525  rp-isfinite6  43531  pr2cv  43561  iunrelexp0  43715  relexpss1d  43718  relexpmulg  43723  iunrelexpmin2  43725  relexp01min  43726  relexp0a  43729  relexpxpmin  43730  relexpaddss  43731  clsk1indlem3  44056  ssrecnpr  44327  seff  44328  sblpnf  44329  expgrowthi  44352  dvconstbi  44353  19.33-2  44401  ax6e2ndeq  44579  en3lpVD  44865  undif3VD  44902  ax6e2ndeqVD  44929  ax6e2ndeqALT  44951  iooinlbub  45514  elprneb  47041  euoreqb  47121  2reu3  47122  afvpcfv0  47158  afvfv0bi  47164  afvco2  47188  afv2orxorb  47240  afv2ndeffv0  47272  afv2fv0b  47278  fvmptrabdm  47305  minusmodnep2tmod  47355  iccpartltu  47412  iccpartgtl  47413  iccpartgt  47414  iccpartleu  47415  iccpartgel  47416  iccpartnel  47425  elsprel  47462  prsprel  47474  sprsymrelfolem2  47480  paireqne  47498  odz2prm2pw  47550  fmtnofac1  47557  fmtno4prmfac  47559  31prm  47584  lighneallem2  47593  lighneallem3  47594  lighneallem4b  47596  lighneallem4  47597  zeo2ALTV  47658  nn0o1gt2ALTV  47681  nn0oALTV  47683  stgoldbwt  47763  sbgoldbwt  47764  sbgoldbalt  47768  sbgoldbm  47771  sbgoldbo  47774  nnsum3primesle9  47781  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  bgoldbtbndlem1  47792  bgoldbtbnd  47796  tgoldbach  47804  vopnbgrelself  47841  clnbgrgrim  47902  grtriproplem  47906  grtrif1o  47909  grtriclwlk3  47912  2ltceilhalf  48015  gpgedgvtx0  48019  gpgcubic  48035  gpg5nbgr3star  48037  upgrwlkupwlk  48056  ztprmneprm  48263  islinindfis  48366  lindslinindsimp2lem5  48379  lindslinindsimp2  48380  lindsrng01  48385  elfzolborelfzop1  48436  flnn0div2ge  48454  blennn0elnn  48498  blen1b  48509  nnolog2flm1  48511  blengt1fldiv2p1  48514  0dig2pr01  48531  dignn0flhalf  48539  nn0sumshdiglemB  48541  nn0sumshdiglem1  48542  resum2sqorgt0  48630  rrx2xpref1o  48639  rrx2plord2  48643  itsclc0yqsol  48685  mosssn  48734  mo0sn  48735  mofsssn  48755  mofmo  48756  f1omo  48792