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  1025  ecase3  1048  cases2ALT  1064  consensus  1068  jaoi3  1076  1fpid3  1098  19.33  1914  19.33b  1915  nfim1  2235  dfsb2  2525  mooran1  2583  eueq3  3674  sbcor  3794  sspss  4056  sspsstr  4063  elun  4107  ssun  4148  inss  4201  raaan2  4483  ifbi  4510  ifcomnan  4544  rabsnifsb  4688  tpprceq3  4772  tppreqb  4773  pwpw0  4779  sssn  4792  snsssn  4806  preq12b  4815  prnebg  4821  preq12nebg  4828  elpr2elpr  4834  prproe  4870  3elpr2eq  4871  unissint  4937  zfpair  5392  axprg  5408  propeqop  5490  propssopi  5491  opthhausdorff  5500  opthhausdorff0  5501  iunopeqop  5504  iunopeqopOLD  5505  relsnb  5789  iresn0n0  6056  sotri2  6129  sotri3  6130  somincom  6134  ordssun  6465  unizlim  6485  onxpdisj  6488  tpres  7199  sorpssuni  7729  ordeleqon  7777  ordunisuc  7824  orduninsuc  7835  tfinds  7852  limomss  7863  limom  7874  soxp  8121  ressuppssdif  8177  tfr2b  8379  omopthi  8643  domnsym  9087  ordfin  9196  brwdom  9525  cantnfvalf  9630  ttrclselem1  9690  djuss  9902  djuunxp  9903  eldju2ndl  9906  eldju2ndr  9907  djuun  9908  updjud  9916  iscard3  10073  cflim2  10242  sornom  10256  isfin5  10278  isfin6  10279  sdom2en01  10281  fin23lem29  10320  fin23lem30  10321  fin56  10372  fin67  10374  hsmexlem9  10404  axcc4dom  10420  axdc3lem2  10430  axdc3lem4  10432  brdom3  10507  winainflem  10673  r1tskina  10762  indpi  10887  ltxrlt  11275  nn0sub  12549  nn0n0n1ge2b  12568  nn0ge2m1nn  12569  xnn0xr  12577  xnn0nemnf  12583  elnn0z  12599  nn0lt10b  12653  nn0le2is012  12655  nn0ind-raph  12691  uzin  12893  indstr2  12946  nn0ledivnn  13126  xrnemnf  13137  xrnepnf  13138  mnfltxr  13147  xnn0n0n1ge2b  13152  xnn0ge0  13154  xnn0xaddcl  13256  xnn0lenn0nn0  13266  xnn0xadd0  13268  xmullem2  13286  rexmul  13292  xnn0xrge0  13528  elfzonlteqm1  13766  elfznelfzo  13798  injresinjlem  13815  injresinj  13816  fldiv4p1lem1div2  13864  fldiv4lem1div2  13866  modfzo0difsn  13975  ssnn0fi  14017  fsuppmapnn0fiubex  14024  m1expcl2  14117  m1expeven  14141  zzlesq  14238  sq01  14257  expnngt1  14273  nn0opthi  14302  facp1  14310  faclbnd3  14324  faclbnd4lem1  14325  faclbnd4lem3  14327  bcn1  14345  hashnemnf  14376  hashv01gt1  14377  hashneq0  14396  hashrabrsn  14404  hashrabsn01  14405  hashrabsn1  14406  hashunx  14418  hashsnle1  14450  hashfzp1  14464  hash2pwpr  14509  hashge2el2difr  14514  swrdnd2  14689  pfxnd0  14722  repswswrd  14817  relexpsucl  15064  relexpsucr  15065  relexpcnv  15068  relexprelg  15071  relexpdmg  15075  relexprng  15079  relexpfld  15082  relexpaddg  15086  sumz  15769  arisum  15910  arisum2  15911  pwdif  15918  ntrivcvg  15947  prod1  15994  fprodfac  16023  mod2eq1n2dvds  16400  mulsucdiv2z  16406  nn0o1gt2  16434  nno  16435  nn0o  16436  sumeven  16440  sumodd  16441  divalglem1  16447  divalglem6  16451  gcdaddmlem  16577  dfgcd2  16599  mulgcd  16601  lcmf  16686  lcmfunsnlem2lem2  16692  lcmfunsnlem2  16693  prm2orodd  16744  dfphi2  16828  nnnn0modprm0  16861  prm23lt5  16869  oddprmdvds  16958  4sqlem19  17018  ramz  17080  prmolefac  17101  prmgaplem7  17112  cshwshashlem1  17150  ressval3d  17301  firest  17480  xpsfeq  17612  funcres2c  17955  ex-chn2  18689  smndex1basss  18962  smndex1mgm  18964  smndex1mndlem  18966  mulgnn0gsum  19141  symgfix2  19481  pmtrprfval  19552  m1expaddsub  19563  psgnprfval  19586  gsumpr  20020  gsumzunsnd  20021  0ringnnzr  20623  isfieldidl  21386  frgpcyg  21723  cnmsgnsubg  21727  psgninv  21732  zrhpsgnelbas  21744  m2detleiblem1  22781  symgmatr01lem  22810  indiscld  23248  pnfnei  23377  mnfnei  23378  alexsubALTlem2  24205  alexsubALTlem3  24206  dscmet  24729  xrtgioo  24964  ishl2  25529  iunmbl2  25716  icombl  25723  ioombl  25724  recnprss  26063  recnperf  26064  dvexp2  26113  dvexp3  26137  dvne0f1  26171  plypf1  26369  taylfvallem1  26520  taylfval  26522  tayl0  26525  coseq0negpitopi  26668  logfac  26766  cxpexp  26833  pythag  26982  reasinsin  27061  harmonicbnd3  27172  lgslem4  27464  gausslemma2dlem0i  27528  lgsquadlem2  27545  2lgslem3  27568  2lgs  27571  2lgsoddprmlem3  27578  2sqnn0  27602  2sqnn  27603  ltsres  27826  nolesgn2o  27835  nogesgn1o  27837  nosep1o  27845  nosep2o  27846  noetalem2  27906  sltsun1  27981  sltsun2  27982  eln0s  28554  n0zs  28582  bdaypw2n0bndlem  28656  bdaypw2n0bnd  28657  lfgrnloop  29475  uhgr2edg  29558  usgredg4  29567  usgredg2v  29577  usgrexmplef  29609  nb3grprlem1  29730  uvtx01vtx  29747  wlk1walk  29988  upgriswlk  29990  pthdadjvtx  30077  upgrwlkdvdelem  30085  pthdlem2lem  30116  pthspthcyc  30152  2pthon3v  30292  clwwlkn  30377  clwwlkneq0  30380  eupth2lem3lem4  30582  konigsberg  30608  3vfriswmgrlem  30628  1to2vfriswmgr  30630  1to3vfriswmgr  30631  frgrregorufr0  30675  numclwlk1  30722  ex-pr  30781  shunssi  31720  cvmdi  32676  1neg1t1neg1  33083  iundisj2cnt  33144  fz1nnct  33146  xrge0iifiso  34325  esumpr2  34457  measiuns  34607  sxbrsigalem0  34661  bnj964  35331  subfacval3  35681  kur14lem7  35704  satfrnmapom  35862  gonar  35887  goalr  35889  mrsubcv  36002  nepss  36210  nnuni  36219  fz0n  36223  bccolsum  36231  dfon2lem7  36279  altopthsn  36453  elhf2  36667  nn0prpw  36834  dissym1  36932  ordcmp  36958  ttciunun  37022  bj-currypeirce  37149  bj-jaoi1  37164  bj-jaoi2  37165  bj-ififc  37175  bj-andnotim  37181  bj-nfimexal  37231  bj-sbsb  37472  bj-elsn12g  37696  bj-ideqg1  37808  finxpreclem2  38036  wl-equsal1i  38199  tan2h  38263  poimirlem23  38294  poimirlem32  38303  itg2addnclem  38322  orfa1  38736  orfa2  38737  inex3  38987  inxpex  38988  mopickr  39020  disjlem14  39550  elpadd0  40583  aks6d1c2p2  42886  quadfac  42972  sbor2  42981  sn-0ne2  43167  sn-0lt1  43249  hbtlem5  43855  omabs2  44059  safesnsupfiss  44141  safesnsupfidom1o  44143  safesnsupfilb  44144  rp-fakeimass  44238  rp-isfinite6  44244  pr2cv  44274  iunrelexp0  44428  relexpss1d  44431  relexpmulg  44436  iunrelexpmin2  44438  relexp01min  44439  relexp0a  44442  relexpxpmin  44443  relexpaddss  44444  clsk1indlem3  44769  ssrecnpr  45018  seff  45019  sblpnf  45020  expgrowthi  45043  dvconstbi  45044  19.33-2  45092  ax6e2ndeq  45268  en3lpVD  45553  undif3VD  45590  ax6e2ndeqVD  45617  ax6e2ndeqALT  45639  iooinlbub  46217  elprneb  47766  euoreqb  47846  2reu3  47847  afvpcfv0  47883  afvfv0bi  47889  afvco2  47913  afv2orxorb  47965  afv2ndeffv0  47997  afv2fv0b  48003  fvmptrabdm  48030  nnmul2  48067  2ltceilhalf  48069  ceilhalfnn  48077  minusmodnep2tmod  48096  iccpartltu  48174  iccpartgtl  48175  iccpartgt  48176  iccpartleu  48177  iccpartgel  48178  iccpartnel  48187  elsprel  48224  prsprel  48236  sprsymrelfolem2  48242  paireqne  48260  odz2prm2pw  48315  fmtnofac1  48322  fmtno4prmfac  48324  31prm  48349  lighneallem2  48358  lighneallem3  48359  lighneallem4b  48361  lighneallem4  48362  ppivalnnnprm  48380  ppivalnn  48384  zeo2ALTV  48436  nn0o1gt2ALTV  48459  nn0oALTV  48461  stgoldbwt  48541  sbgoldbwt  48542  sbgoldbalt  48546  sbgoldbm  48549  sbgoldbo  48552  nnsum3primesle9  48559  nnsum4primeseven  48565  nnsum4primesevenALTV  48566  wtgoldbnnsum4prm  48567  bgoldbnnsum3prm  48569  bgoldbtbndlem1  48570  bgoldbtbnd  48574  tgoldbach  48582  vopnbgrelself  48620  clnbgrgrim  48699  grtriproplem  48704  grtrif1o  48707  grtriclwlk3  48710  gpgedgvtx0  48826  gpgcubic  48844  gpg5nbgr3star  48846  gpgprismgr4cycllem3  48862  gpgprismgr4cycllem7  48866  gpgprismgr4cycllem10  48869  pgnbgreunbgrlem3  48883  pgnbgreunbgrlem6  48889  pgnbgreunbgr  48890  upgrwlkupwlk  48905  ztprmneprm  49127  islinindfis  49229  lindslinindsimp2lem5  49242  lindslinindsimp2  49243  lindsrng01  49248  elfzolborelfzop1  49299  flnn0div2ge  49313  blennn0elnn  49357  blen1b  49368  nnolog2flm1  49370  blengt1fldiv2p1  49373  0dig2pr01  49390  dignn0flhalf  49398  nn0sumshdiglemB  49400  nn0sumshdiglem1  49401  resum2sqorgt0  49489  rrx2xpref1o  49498  rrx2plord2  49502  itsclc0yqsol  49544  mosssn  49593  mo0sn  49594  mofsssn  49624  mofmo  49625  f1omo  49671  f1omoOLD  49672