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  1886  19.33b  1887  nfim1  2207  dfsb2  2497  mooran1  2555  eueq3  3657  sbcor  3779  sspss  4042  sspsstr  4048  elun  4093  ssun  4135  inss  4188  raaan2  4462  ifbi  4489  ifcomnan  4523  rabsnifsb  4666  tpprceq3  4749  tppreqb  4750  pwpw0  4756  sssn  4769  snsssn  4784  preq12b  4793  prnebg  4799  preq12nebg  4806  elpr2elpr  4812  prproe  4848  3elpr2eq  4849  unissint  4914  zfpair  5363  axprg  5379  propeqop  5461  propssopi  5462  opthhausdorff  5471  opthhausdorff0  5472  iunopeqop  5475  iunopeqopOLD  5476  relsnb  5758  iresn0n0  6019  sotri2  6092  sotri3  6093  somincom  6097  ordssun  6427  unizlim  6447  onxpdisj  6450  tpres  7156  sorpssuni  7686  ordeleqon  7736  ordunisuc  7783  orduninsuc  7794  tfinds  7811  limomss  7822  limom  7833  soxp  8079  ressuppssdif  8135  tfr2b  8335  omopthi  8597  domnsym  9041  ordfin  9150  brwdom  9482  cantnfvalf  9586  ttrclselem1  9646  djuss  9844  djuunxp  9845  eldju2ndl  9848  eldju2ndr  9849  djuun  9850  updjud  9858  iscard3  10015  cflim2  10185  sornom  10199  isfin5  10221  isfin6  10222  sdom2en01  10224  fin23lem29  10263  fin23lem30  10264  fin56  10315  fin67  10317  hsmexlem9  10347  axcc4dom  10363  axdc3lem2  10373  axdc3lem4  10375  brdom3  10450  winainflem  10616  r1tskina  10705  indpi  10830  ltxrlt  11216  nn0sub  12487  nn0n0n1ge2b  12506  nn0ge2m1nn  12507  xnn0xr  12515  xnn0nemnf  12521  elnn0z  12537  nn0lt10b  12591  nn0le2is012  12593  nn0ind-raph  12629  uzin  12824  indstr2  12877  nn0ledivnn  13057  xrnemnf  13068  xrnepnf  13069  mnfltxr  13078  xnn0n0n1ge2b  13083  xnn0ge0  13085  xnn0xaddcl  13187  xnn0lenn0nn0  13197  xnn0xadd0  13199  xmullem2  13217  rexmul  13223  xnn0xrge0  13459  elfzonlteqm1  13696  elfznelfzo  13728  injresinjlem  13745  injresinj  13746  fldiv4p1lem1div2  13794  fldiv4lem1div2  13796  modfzo0difsn  13905  ssnn0fi  13947  fsuppmapnn0fiubex  13954  m1expcl2  14047  m1expeven  14071  zzlesq  14168  sq01  14187  expnngt1  14203  nn0opthi  14232  facp1  14240  faclbnd3  14254  faclbnd4lem1  14255  faclbnd4lem3  14257  bcn1  14275  hashnemnf  14306  hashv01gt1  14307  hashneq0  14326  hashrabrsn  14334  hashrabsn01  14335  hashrabsn1  14336  hashunx  14348  hashsnle1  14379  hashfzp1  14393  hash2pwpr  14438  hashge2el2difr  14443  swrdnd2  14618  pfxnd0  14651  repswswrd  14746  relexpsucl  14993  relexpsucr  14994  relexpcnv  14997  relexprelg  15000  relexpdmg  15004  relexprng  15008  relexpfld  15011  relexpaddg  15015  sumz  15684  arisum  15825  arisum2  15826  pwdif  15833  ntrivcvg  15862  prod1  15909  fprodfac  15938  mod2eq1n2dvds  16316  mulsucdiv2z  16322  nn0o1gt2  16350  nno  16351  nn0o  16352  sumeven  16356  sumodd  16357  divalglem1  16363  divalglem6  16367  gcdaddmlem  16493  dfgcd2  16515  mulgcd  16517  lcmf  16602  lcmfunsnlem2lem2  16608  lcmfunsnlem2  16609  prm2orodd  16660  dfphi2  16744  nnnn0modprm0  16777  prm23lt5  16785  oddprmdvds  16874  4sqlem19  16934  ramz  16996  prmolefac  17017  prmgaplem7  17028  cshwshashlem1  17066  ressval3d  17216  firest  17395  xpsfeq  17527  funcres2c  17870  ex-chn2  18604  smndex1basss  18876  smndex1mgm  18878  smndex1mndlem  18880  mulgnn0gsum  19056  symgfix2  19391  pmtrprfval  19462  m1expaddsub  19473  psgnprfval  19496  gsumpr  19930  gsumzunsnd  19931  0ringnnzr  20502  frgpcyg  21553  cnmsgnsubg  21557  psgninv  21562  zrhpsgnelbas  21574  m2detleiblem1  22589  symgmatr01lem  22618  indiscld  23056  pnfnei  23185  mnfnei  23186  alexsubALTlem2  24013  alexsubALTlem3  24014  dscmet  24537  xrtgioo  24772  ishl2  25337  iunmbl2  25524  icombl  25531  ioombl  25532  recnprss  25871  recnperf  25872  dvexp2  25921  dvexp3  25945  dvne0f1  25979  plypf1  26177  taylfvallem1  26322  taylfval  26324  tayl0  26327  coseq0negpitopi  26467  logfac  26565  cxpexp  26632  pythag  26781  reasinsin  26860  harmonicbnd3  26971  lgslem4  27263  gausslemma2dlem0i  27327  lgsquadlem2  27344  2lgslem3  27367  2lgs  27370  2lgsoddprmlem3  27377  2sqnn0  27401  2sqnn  27402  ltsres  27626  nolesgn2o  27635  nogesgn1o  27637  nosep1o  27645  nosep2o  27646  noetalem2  27706  sltsun1  27780  sltsun2  27781  eln0s  28353  n0zs  28381  bdaypw2n0bndlem  28455  bdaypw2n0bnd  28456  lfgrnloop  29194  uhgr2edg  29277  usgredg4  29286  usgredg2v  29296  usgrexmplef  29328  nb3grprlem1  29449  uvtx01vtx  29466  wlk1walk  29707  upgriswlk  29709  pthdadjvtx  29796  upgrwlkdvdelem  29804  pthdlem2lem  29835  pthspthcyc  29871  2pthon3v  30011  clwwlkn  30096  clwwlkneq0  30099  eupth2lem3lem4  30301  konigsberg  30327  3vfriswmgrlem  30347  1to2vfriswmgr  30349  1to3vfriswmgr  30350  frgrregorufr0  30394  numclwlk1  30441  ex-pr  30500  shunssi  31439  cvmdi  32395  1neg1t1neg1  32811  iundisj2cnt  32872  fz1nnct  32874  xrge0iifiso  34079  esumpr2  34211  measiuns  34361  sxbrsigalem0  34415  bnj964  35085  subfacval3  35371  kur14lem7  35394  satfrnmapom  35552  gonar  35577  goalr  35579  mrsubcv  35692  nepss  35900  nnuni  35909  fz0n  35913  bccolsum  35921  dfon2lem7  35969  altopthsn  36143  elhf2  36357  nn0prpw  36505  dissym1  36603  ordcmp  36629  ttciunun  36693  bj-currypeirce  36821  bj-jaoi1  36836  bj-jaoi2  36837  bj-ififc  36847  bj-andnotim  36853  bj-nfimexal  36903  bj-sbsb  37144  bj-elsn12g  37367  bj-ideqg1  37478  finxpreclem2  37706  wl-equsal1i  37869  tan2h  37933  poimirlem23  37964  poimirlem32  37973  itg2addnclem  37992  orfa1  38406  orfa2  38407  inex3  38659  inxpex  38660  mopickr  38692  disjlem14  39222  elpadd0  40255  aks6d1c2p2  42558  sbor2  42651  sn-0ne2  42838  sn-0lt1  42920  hbtlem5  43556  omabs2  43760  safesnsupfiss  43842  safesnsupfidom1o  43844  safesnsupfilb  43845  rp-fakeimass  43939  rp-isfinite6  43945  pr2cv  43975  iunrelexp0  44129  relexpss1d  44132  relexpmulg  44137  iunrelexpmin2  44139  relexp01min  44140  relexp0a  44143  relexpxpmin  44144  relexpaddss  44145  clsk1indlem3  44470  ssrecnpr  44735  seff  44736  sblpnf  44737  expgrowthi  44760  dvconstbi  44761  19.33-2  44809  ax6e2ndeq  44986  en3lpVD  45271  undif3VD  45308  ax6e2ndeqVD  45335  ax6e2ndeqALT  45357  iooinlbub  45931  elprneb  47477  euoreqb  47557  2reu3  47558  afvpcfv0  47594  afvfv0bi  47600  afvco2  47624  afv2orxorb  47676  afv2ndeffv0  47708  afv2fv0b  47714  fvmptrabdm  47741  nnmul2  47778  2ltceilhalf  47780  ceilhalfnn  47788  minusmodnep2tmod  47807  iccpartltu  47885  iccpartgtl  47886  iccpartgt  47887  iccpartleu  47888  iccpartgel  47889  iccpartnel  47898  elsprel  47935  prsprel  47947  sprsymrelfolem2  47953  paireqne  47971  odz2prm2pw  48026  fmtnofac1  48033  fmtno4prmfac  48035  31prm  48060  lighneallem2  48069  lighneallem3  48070  lighneallem4b  48072  lighneallem4  48073  ppivalnnnprm  48091  ppivalnn  48095  zeo2ALTV  48147  nn0o1gt2ALTV  48170  nn0oALTV  48172  stgoldbwt  48252  sbgoldbwt  48253  sbgoldbalt  48257  sbgoldbm  48260  sbgoldbo  48263  nnsum3primesle9  48270  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  bgoldbtbndlem1  48281  bgoldbtbnd  48285  tgoldbach  48293  vopnbgrelself  48331  clnbgrgrim  48410  grtriproplem  48415  grtrif1o  48418  grtriclwlk3  48421  gpgedgvtx0  48537  gpgcubic  48555  gpg5nbgr3star  48557  gpgprismgr4cycllem3  48573  gpgprismgr4cycllem7  48577  gpgprismgr4cycllem10  48580  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem6  48600  pgnbgreunbgr  48601  upgrwlkupwlk  48616  ztprmneprm  48823  islinindfis  48925  lindslinindsimp2lem5  48938  lindslinindsimp2  48939  lindsrng01  48944  elfzolborelfzop1  48995  flnn0div2ge  49009  blennn0elnn  49053  blen1b  49064  nnolog2flm1  49066  blengt1fldiv2p1  49069  0dig2pr01  49086  dignn0flhalf  49094  nn0sumshdiglemB  49096  nn0sumshdiglem1  49097  resum2sqorgt0  49185  rrx2xpref1o  49194  rrx2plord2  49198  itsclc0yqsol  49240  mosssn  49290  mo0sn  49291  mofsssn  49321  mofmo  49322  f1omo  49368  f1omoOLD  49369