Theorem jaoi 870

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 864	. . 3 ⊢ ((𝜑 ∨ 𝜒) → (¬ 𝜑 → 𝜒))
2		jaoi.2	. . 3 ⊢ (𝜒 → 𝜓)
3	1, 2	syl6 36	. 2 ⊢ ((𝜑 ∨ 𝜒) → (¬ 𝜑 → 𝜓))
4		jaoi.1	. 2 ⊢ (𝜑 → 𝜓)
5	3, 4	pm2.61d2 183	1 ⊢ ((𝜑 ∨ 𝜒) → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  jao1i  871  jaod  872  pm1.4  882  pm3.2ni  893  pm1.2  916  pm2.4  919  pm2.41  920  orim12i  921  pm1.5  932  pm2.42  957  jaoa  970  jaoian  971  pm4.44  1012  andi  1023  ecase3  1046  cases2ALT  1062  consensus  1066  jaoi3  1074  1fpid3  1096  19.33  1911  19.33b  1912  nfim1  2241  dfsb2  2531  mooran1  2589  eueq3  3683  sbcor  3803  sspss  4064  sspsstr  4071  elun  4115  ssun  4156  inss  4209  raaan2  4488  ifbi  4515  ifcomnan  4549  rabsnifsb  4693  tpprceq3  4776  tppreqb  4777  pwpw0  4783  sssn  4796  snsssn  4810  preq12b  4819  prnebg  4825  preq12nebg  4832  elpr2elpr  4838  prproe  4874  3elpr2eq  4875  unissint  4941  zfpair  5393  axprg  5409  propeqop  5491  propssopi  5492  opthhausdorff  5501  opthhausdorff0  5502  iunopeqop  5505  iunopeqopOLD  5506  relsnb  5790  iresn0n0  6057  sotri2  6130  sotri3  6131  somincom  6135  ordssun  6466  unizlim  6486  onxpdisj  6489  tpres  7200  sorpssuni  7730  ordeleqon  7780  ordunisuc  7827  orduninsuc  7838  tfinds  7855  limomss  7866  limom  7877  soxp  8124  ressuppssdif  8180  tfr2b  8382  omopthi  8646  domnsym  9090  ordfin  9199  brwdom  9528  cantnfvalf  9633  ttrclselem1  9693  djuss  9905  djuunxp  9906  eldju2ndl  9909  eldju2ndr  9910  djuun  9911  updjud  9919  iscard3  10076  cflim2  10246  sornom  10260  isfin5  10282  isfin6  10283  sdom2en01  10285  fin23lem29  10324  fin23lem30  10325  fin56  10376  fin67  10378  hsmexlem9  10408  axcc4dom  10424  axdc3lem2  10434  axdc3lem4  10436  brdom3  10511  winainflem  10677  r1tskina  10766  indpi  10891  ltxrlt  11279  nn0sub  12553  nn0n0n1ge2b  12572  nn0ge2m1nn  12573  xnn0xr  12581  xnn0nemnf  12587  elnn0z  12603  nn0lt10b  12657  nn0le2is012  12659  nn0ind-raph  12695  uzin  12897  indstr2  12950  nn0ledivnn  13130  xrnemnf  13141  xrnepnf  13142  mnfltxr  13151  xnn0n0n1ge2b  13156  xnn0ge0  13158  xnn0xaddcl  13260  xnn0lenn0nn0  13270  xnn0xadd0  13272  xmullem2  13290  rexmul  13296  xnn0xrge0  13532  elfzonlteqm1  13769  elfznelfzo  13801  injresinjlem  13818  injresinj  13819  fldiv4p1lem1div2  13867  fldiv4lem1div2  13869  modfzo0difsn  13978  ssnn0fi  14020  fsuppmapnn0fiubex  14027  m1expcl2  14120  m1expeven  14144  zzlesq  14241  sq01  14260  expnngt1  14276  nn0opthi  14305  facp1  14313  faclbnd3  14327  faclbnd4lem1  14328  faclbnd4lem3  14330  bcn1  14348  hashnemnf  14379  hashv01gt1  14380  hashneq0  14399  hashrabrsn  14407  hashrabsn01  14408  hashrabsn1  14409  hashunx  14421  hashsnle1  14453  hashfzp1  14467  hash2pwpr  14512  hashge2el2difr  14517  swrdnd2  14692  pfxnd0  14725  repswswrd  14820  relexpsucl  15067  relexpsucr  15068  relexpcnv  15071  relexprelg  15074  relexpdmg  15078  relexprng  15082  relexpfld  15085  relexpaddg  15089  sumz  15772  arisum  15913  arisum2  15914  pwdif  15921  ntrivcvg  15950  prod1  15997  fprodfac  16026  mod2eq1n2dvds  16404  mulsucdiv2z  16410  nn0o1gt2  16438  nno  16439  nn0o  16440  sumeven  16444  sumodd  16445  divalglem1  16451  divalglem6  16455  gcdaddmlem  16581  dfgcd2  16603  mulgcd  16605  lcmf  16690  lcmfunsnlem2lem2  16696  lcmfunsnlem2  16697  prm2orodd  16748  dfphi2  16832  nnnn0modprm0  16865  prm23lt5  16873  oddprmdvds  16962  4sqlem19  17022  ramz  17084  prmolefac  17105  prmgaplem7  17116  cshwshashlem1  17154  ressval3d  17305  firest  17484  xpsfeq  17616  funcres2c  17959  ex-chn2  18693  smndex1basss  18966  smndex1mgm  18968  smndex1mndlem  18970  mulgnn0gsum  19145  symgfix2  19485  pmtrprfval  19556  m1expaddsub  19567  psgnprfval  19590  gsumpr  20024  gsumzunsnd  20025  0ringnnzr  20608  frgpcyg  21691  cnmsgnsubg  21695  psgninv  21700  zrhpsgnelbas  21712  m2detleiblem1  22749  symgmatr01lem  22778  indiscld  23216  pnfnei  23345  mnfnei  23346  alexsubALTlem2  24173  alexsubALTlem3  24174  dscmet  24697  xrtgioo  24932  ishl2  25497  iunmbl2  25684  icombl  25691  ioombl  25692  recnprss  26031  recnperf  26032  dvexp2  26081  dvexp3  26105  dvne0f1  26139  plypf1  26337  taylfvallem1  26485  taylfval  26487  tayl0  26490  coseq0negpitopi  26633  logfac  26731  cxpexp  26798  pythag  26947  reasinsin  27026  harmonicbnd3  27137  lgslem4  27429  gausslemma2dlem0i  27493  lgsquadlem2  27510  2lgslem3  27533  2lgs  27536  2lgsoddprmlem3  27543  2sqnn0  27567  2sqnn  27568  ltsres  27791  nolesgn2o  27800  nogesgn1o  27802  nosep1o  27810  nosep2o  27811  noetalem2  27871  sltsun1  27946  sltsun2  27947  eln0s  28519  n0zs  28547  bdaypw2n0bndlem  28621  bdaypw2n0bnd  28622  lfgrnloop  29415  uhgr2edg  29498  usgredg4  29507  usgredg2v  29517  usgrexmplef  29549  nb3grprlem1  29670  uvtx01vtx  29687  wlk1walk  29928  upgriswlk  29930  pthdadjvtx  30017  upgrwlkdvdelem  30025  pthdlem2lem  30056  pthspthcyc  30092  2pthon3v  30232  clwwlkn  30317  clwwlkneq0  30320  eupth2lem3lem4  30522  konigsberg  30548  3vfriswmgrlem  30568  1to2vfriswmgr  30570  1to3vfriswmgr  30571  frgrregorufr0  30615  numclwlk1  30662  ex-pr  30721  shunssi  31660  cvmdi  32616  1neg1t1neg1  33023  iundisj2cnt  33084  fz1nnct  33086  xrge0iifiso  34269  esumpr2  34401  measiuns  34551  sxbrsigalem0  34605  bnj964  35275  subfacval3  35579  kur14lem7  35602  satfrnmapom  35760  gonar  35785  goalr  35787  mrsubcv  35900  nepss  36108  nnuni  36117  fz0n  36121  bccolsum  36129  dfon2lem7  36177  altopthsn  36351  elhf2  36565  nn0prpw  36722  dissym1  36820  ordcmp  36846  ttciunun  36910  bj-currypeirce  37037  bj-jaoi1  37052  bj-jaoi2  37053  bj-ififc  37063  bj-andnotim  37069  bj-nfimexal  37119  bj-sbsb  37360  bj-elsn12g  37583  bj-ideqg1  37695  finxpreclem2  37923  wl-equsal1i  38086  tan2h  38150  poimirlem23  38181  poimirlem32  38190  itg2addnclem  38209  orfa1  38623  orfa2  38624  inex3  38876  inxpex  38877  mopickr  38909  disjlem14  39439  elpadd0  40472  aks6d1c2p2  42775  quadfac  42861  sbor2  42870  sn-0ne2  43056  sn-0lt1  43138  hbtlem5  43746  omabs2  43950  safesnsupfiss  44032  safesnsupfidom1o  44034  safesnsupfilb  44035  rp-fakeimass  44129  rp-isfinite6  44135  pr2cv  44165  iunrelexp0  44319  relexpss1d  44322  relexpmulg  44327  iunrelexpmin2  44329  relexp01min  44330  relexp0a  44333  relexpxpmin  44334  relexpaddss  44335  clsk1indlem3  44660  ssrecnpr  44909  seff  44910  sblpnf  44911  expgrowthi  44934  dvconstbi  44935  19.33-2  44983  ax6e2ndeq  45159  en3lpVD  45444  undif3VD  45481  ax6e2ndeqVD  45508  ax6e2ndeqALT  45530  iooinlbub  46108  elprneb  47654  euoreqb  47734  2reu3  47735  afvpcfv0  47771  afvfv0bi  47777  afvco2  47801  afv2orxorb  47853  afv2ndeffv0  47885  afv2fv0b  47891  fvmptrabdm  47918  nnmul2  47955  2ltceilhalf  47957  ceilhalfnn  47965  minusmodnep2tmod  47984  iccpartltu  48062  iccpartgtl  48063  iccpartgt  48064  iccpartleu  48065  iccpartgel  48066  iccpartnel  48075  elsprel  48112  prsprel  48124  sprsymrelfolem2  48130  paireqne  48148  odz2prm2pw  48203  fmtnofac1  48210  fmtno4prmfac  48212  31prm  48237  lighneallem2  48246  lighneallem3  48247  lighneallem4b  48249  lighneallem4  48250  ppivalnnnprm  48268  ppivalnn  48272  zeo2ALTV  48324  nn0o1gt2ALTV  48347  nn0oALTV  48349  stgoldbwt  48429  sbgoldbwt  48430  sbgoldbalt  48434  sbgoldbm  48437  sbgoldbo  48440  nnsum3primesle9  48447  nnsum4primeseven  48453  nnsum4primesevenALTV  48454  wtgoldbnnsum4prm  48455  bgoldbnnsum3prm  48457  bgoldbtbndlem1  48458  bgoldbtbnd  48462  tgoldbach  48470  vopnbgrelself  48508  clnbgrgrim  48587  grtriproplem  48592  grtrif1o  48595  grtriclwlk3  48598  gpgedgvtx0  48714  gpgcubic  48732  gpg5nbgr3star  48734  gpgprismgr4cycllem3  48750  gpgprismgr4cycllem7  48754  gpgprismgr4cycllem10  48757  pgnbgreunbgrlem3  48771  pgnbgreunbgrlem6  48777  pgnbgreunbgr  48778  upgrwlkupwlk  48793  ztprmneprm  49011  islinindfis  49113  lindslinindsimp2lem5  49126  lindslinindsimp2  49127  lindsrng01  49132  elfzolborelfzop1  49183  flnn0div2ge  49197  blennn0elnn  49241  blen1b  49252  nnolog2flm1  49254  blengt1fldiv2p1  49257  0dig2pr01  49274  dignn0flhalf  49282  nn0sumshdiglemB  49284  nn0sumshdiglem1  49285  resum2sqorgt0  49373  rrx2xpref1o  49382  rrx2plord2  49386  itsclc0yqsol  49428  mosssn  49477  mo0sn  49478  mofsssn  49508  mofmo  49509  f1omo  49555  f1omoOLD  49556