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  1916  19.33b  1917  nfim1  2235  dfsb2  2522  mooran1  2580  eueq3  3668  sbcor  3788  sspss  4028  sspsstr  4035  inss  4144  elun  4151  ssun  4192  raaan2  4477  ifbi  4504  ifcomnan  4538  rabsnifsb  4679  tpprceq3  4763  tppreqb  4764  sssn  4781  snsssn  4795  preq12b  4804  prnebg  4810  preq12nebg  4817  elpr2elpr  4823  pwpw0  4830  prproe  4832  3elpr2eq  4833  unissint  4931  zfpair  5383  axprg  5395  propeqop  5479  propssopi  5480  opthhausdorff  5490  opthhausdorff0  5491  iunopeqop  5494  iunopeqopOLD  5495  relsnb  5781  iresn0n0  6048  sotri2  6125  sotri3  6126  somincom  6130  ordssun  6470  unizlim  6490  onxpdisj  6493  tpres  7211  sorpssuni  7752  ordeleqon  7800  ordunisuc  7847  orduninsuc  7858  tfinds  7875  limomss  7886  limom  7897  soxp  8147  ressuppssdif  8209  tfr2b  8411  omopthi  8677  domnsym  9129  ordfin  9238  brwdom  9568  cantnfvalf  9673  ttrclselem1  9733  elhf2  9917  djuss  10008  djuunxp  10009  eldju2ndl  10012  eldju2ndr  10013  djuun  10014  updjud  10022  iscard3  10179  cflim2  10348  sornom  10362  isfin5  10384  isfin6  10385  sdom2en01  10387  fin23lem29  10426  fin23lem30  10427  fin56  10478  fin67  10480  hsmexlem9  10510  axcc4dom  10526  axdc3lem2  10536  axdc3lem4  10538  brdom3  10614  winainflem  10785  r1tskina  10874  indpi  10999  ltxrlt  11387  nn0sub  12663  nn0n0n1ge2b  12682  nn0ge2m1nn  12683  xnn0xr  12691  xnn0nemnf  12697  elnn0z  12713  nn0lt10b  12768  nn0le2is012  12770  nn0ind-raph  12806  uzin  13008  indstr2  13061  nn0ledivnn  13242  xrnemnf  13253  xrnepnf  13254  mnfltxr  13263  xnn0n0n1ge2b  13268  xnn0ge0  13270  xnn0xaddcl  13372  xnn0lenn0nn0  13382  xnn0xadd0  13384  xmullem2  13402  rexmul  13408  xnn0xrge0  13644  elfzonlteqm1  13883  elfznelfzo  13915  injresinjlem  13932  injresinj  13933  fldiv4p1lem1div2  13982  fldiv4lem1div2  13984  modfzo0difsn  14093  ssnn0fi  14135  fsuppmapnn0fiubex  14142  m1expcl2  14235  m1expeven  14259  zzlesq  14357  sq01  14376  expnngt1  14392  nn0opthi  14421  facp1  14429  faclbnd3  14443  faclbnd4lem1  14444  faclbnd4lem3  14446  bcn1  14464  hashnemnf  14495  hashv01gt1  14496  hashneq0  14515  hashrabrsn  14523  hashrabsn01  14524  hashrabsn1  14525  hashunx  14537  hashsnle1  14569  hashfzp1  14583  hash2pwpr  14628  hashge2el2difr  14633  swrdnd2  14813  pfxnd0  14846  repswswrd  14943  relexpsucl  15193  relexpsucr  15194  relexpcnv  15197  relexprelg  15200  relexpdmg  15204  relexprng  15208  relexpfld  15211  relexpaddg  15215  sumz  15897  arisum  16038  arisum2  16039  pwdif  16046  ntrivcvg  16075  prod1  16120  fprodfac  16149  mod2eq1n2dvds  16526  mulsucdiv2z  16532  nn0o1gt2  16560  nno  16561  nn0o  16562  sumeven  16566  sumodd  16567  divalglem1  16573  divalglem6  16577  gcdaddmlem  16705  dfgcd2  16728  mulgcd  16730  lcmf  16817  lcmfunsnlem2lem2  16823  lcmfunsnlem2  16824  prm2orodd  16875  dfphi2  16960  nnnn0modprm0  16993  prm23lt5  17001  oddprmdvds  17090  4sqlem19  17150  ramz  17212  prmolefac  17233  prmgaplem7  17244  cshwshashlem1  17282  ressval3d  17433  firest  17612  xpsfeq  17744  funcres2c  18087  ex-chn2  18821  smndex1basss  19113  smndex1mgm  19115  smndex1mndlem  19117  mulgnn0gsum  19299  symgfix2  19639  pmtrprfval  19710  m1expaddsub  19721  psgnprfval  19744  gsumpr  20178  gsumzunsnd  20179  0ringnnzr  20785  isfieldidl  21549  frgpcyg  21888  cnmsgnsubg  21892  psgninv  21897  zrhpsgnelbas  21909  m2detleiblem1  22948  symgmatr01lem  22977  indiscld  23418  pnfnei  23547  mnfnei  23548  alexsubALTlem2  24376  alexsubALTlem3  24377  dscmet  24900  xrtgioo  25135  ishl2  25700  iunmbl2  25887  icombl  25894  ioombl  25895  recnprss  26233  recnperf  26234  dvexp2  26283  dvexp3  26307  dvne0f1  26341  plypf1  26540  taylfvallem1  26693  taylfval  26695  tayl0  26698  coseq0negpitopi  26841  logfac  26938  cxpexp  27005  pythag  27154  reasinsin  27233  harmonicbnd3  27344  lgslem4  27636  gausslemma2dlem0i  27700  lgsquadlem2  27717  2lgslem3  27740  2lgs  27743  2lgsoddprmlem3  27750  2sqnn0  27774  2sqnn  27775  ltsres  28028  nolesgn2o  28037  nogesgn1o  28039  nosep1o  28047  nosep2o  28048  noetalem2  28108  sltsun1  28183  sltsun2  28184  eln0s  28756  n0zs  28784  bdaypw2n0bndlem  28858  bdaypw2n0bnd  28859  lfgrnloop  29712  uhgr2edg  29798  usgredg4  29807  usgredg2v  29817  usgrexmplef  29849  nb3grprlem1  29970  uvtx01vtx  29987  wlk1walk  30228  upgriswlk  30230  pthdadjvtx  30322  upgrwlkdvdelem  30331  pthdlem2lem  30362  pthspthcyc  30400  2pthon3v  30541  clwwlkn  30626  clwwlkneq0  30629  eupth2lem3lem4  30841  konigsberg  30867  3vfriswmgrlem  30887  1to2vfriswmgr  30889  1to3vfriswmgr  30890  frgrregorufr0  30934  numclwlk1  30981  ex-pr  31040  shunssi  31979  cvmdi  32935  1neg1t1neg1  33380  iundisj2cnt  33441  fz1nnct  33443  xrge0iifiso  34617  esumpr2  34749  measiuns  34900  sxbrsigalem0  34953  bnj964  35623  subfacval3  36044  kur14lem7  36067  satfrnmapom  36225  gonar  36250  goalr  36252  mrsubcv  36365  nepss  36579  nnuni  36588  fz0n  36592  bccolsum  36600  dfon2lem7  36647  altopthsn  36822  nn0prpw  37207  dissym1  37305  ordcmp  37331  ttciunun  37395  bj-currypeirce  37522  bj-jaoi1  37537  bj-jaoi2  37538  bj-ififc  37548  bj-andnotim  37554  bj-nfimexal  37604  bj-sbsb  37845  bj-elsn12g  38083  bj-ideqg1  38194  finxpreclem2  38422  wl-equsal1i  38585  tan2h  38644  poimirlem23  38670  poimirlem32  38679  itg2addnclem  38698  dfprop1  38754  orfa1  39128  orfa2  39129  inex3  39379  inxpex  39380  mopickr  39412  disjlem14  39942  elpadd0  40975  aks6d1c2p2  43278  quadfac  43364  sbor2  43373  sn-0ne2  43566  sn-0lt1  43648  hbtlem5  44239  omabs2  44443  safesnsupfiss  44525  safesnsupfidom1o  44527  safesnsupfilb  44528  rp-fakeimass  44622  rp-isfinite6  44628  pr2cv  44658  iunrelexp0  44811  relexpss1d  44814  relexpmulg  44819  iunrelexpmin2  44821  relexp01min  44822  relexp0a  44825  relexpxpmin  44826  relexpaddss  44827  clsk1indlem3  45152  ssrecnpr  45401  seff  45402  sblpnf  45403  expgrowthi  45426  dvconstbi  45427  19.33-2  45475  ax6e2ndeq  45650  en3lpVD  45935  undif3VD  45972  ax6e2ndeqVD  45999  ax6e2ndeqALT  46021  iooinlbub  46621  wrddun  48007  chndun  48012  chnrun  48017  elprneb  48207  euoreqb  48288  2reu3  48289  afvpcfv0  48324  afvfv0bi  48330  afvco2  48354  afv2orxorb  48406  afv2ndeffv0  48438  afv2fv0b  48444  fvmptrabdm  48471  nnmul2  48508  2ltceilhalf  48510  ceilhalfnn  48518  minusmodnep2tmod  48537  iccpartltu  48615  iccpartgtl  48616  iccpartgt  48617  iccpartleu  48618  iccpartgel  48619  iccpartnel  48628  elsprel  48665  prsprel  48677  sprsymrelfolem2  48683  paireqne  48701  odz2prm2pw  48756  fmtnofac1  48763  fmtno4prmfac  48765  31prm  48790  lighneallem2  48799  lighneallem3  48800  lighneallem4b  48802  lighneallem4  48803  ppivalnnnprm  48821  ppivalnn  48825  zeo2ALTV  48877  nn0o1gt2ALTV  48900  nn0oALTV  48902  stgoldbwt  48982  sbgoldbwt  48983  sbgoldbalt  48987  sbgoldbm  48990  sbgoldbo  48993  nnsum3primesle9  49000  nnsum4primeseven  49006  nnsum4primesevenALTV  49007  wtgoldbnnsum4prm  49008  bgoldbnnsum3prm  49010  bgoldbtbndlem1  49011  bgoldbtbnd  49015  tgoldbach  49023  vopnbgrelself  49061  clnbgrgrim  49140  grtriproplem  49145  grtrif1o  49148  grtriclwlk3  49151  gpgedgvtx0  49267  gpgcubic  49285  gpg5nbgr3star  49287  gpgprismgr4cycllem3  49303  gpgprismgr4cycllem7  49307  gpgprismgr4cycllem10  49310  pgnbgreunbgrlem3  49324  pgnbgreunbgrlem6  49330  pgnbgreunbgr  49331  upgrwlkupwlk  49346  ztprmneprm  49567  islinindfis  49669  lindslinindsimp2lem5  49682  lindslinindsimp2  49683  lindsrng01  49688  elfzolborelfzop1  49739  flnn0div2ge  49753  blennn0elnn  49797  blen1b  49808  nnolog2flm1  49810  blengt1fldiv2p1  49813  0dig2pr01  49830  dignn0flhalf  49838  nn0sumshdiglemB  49840  nn0sumshdiglem1  49841  resum2sqorgt0  49929  rrx2plord2  49943  itsclc0yqsol  49984  mosssn  50034  mo0sn  50035  mofsssn  50065  mofmo  50066  f1omo  50115  f1omoOLD  50116  parhomcl2  50853