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  2498  mooran1  2556  eueq3  3671  sbcor  3793  sspss  4056  sspsstr  4062  elun  4107  ssun  4149  inss  4202  raaan2  4477  ifbi  4504  ifcomnan  4538  rabsnifsb  4681  tpprceq3  4762  tppreqb  4763  pwpw0  4771  sssn  4784  snsssn  4799  preq12b  4808  prnebg  4814  preq12nebg  4821  elpr2elpr  4827  prproe  4863  3elpr2eq  4864  unissint  4929  zfpair  5368  axprg  5383  propeqop  5463  propssopi  5464  opthhausdorff  5473  opthhausdorff0  5474  iunopeqop  5477  relsnb  5759  iresn0n0  6021  sotri2  6094  sotri3  6095  somincom  6099  ordssun  6429  unizlim  6449  onxpdisj  6452  tpres  7157  sorpssuni  7687  ordeleqon  7737  ordunisuc  7784  orduninsuc  7795  tfinds  7812  limomss  7823  limom  7834  soxp  8081  ressuppssdif  8137  tfr2b  8337  omopthi  8599  domnsym  9043  ordfin  9152  brwdom  9484  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  11215  nn0sub  12463  nn0n0n1ge2b  12482  nn0ge2m1nn  12483  xnn0xr  12491  xnn0nemnf  12497  elnn0z  12513  nn0lt10b  12566  nn0le2is012  12568  nn0ind-raph  12604  uzin  12799  indstr2  12852  nn0ledivnn  13032  xrnemnf  13043  xrnepnf  13044  mnfltxr  13053  xnn0n0n1ge2b  13058  xnn0ge0  13060  xnn0xaddcl  13162  xnn0lenn0nn0  13172  xnn0xadd0  13174  xmullem2  13192  rexmul  13198  xnn0xrge0  13434  elfzonlteqm1  13669  elfznelfzo  13701  injresinjlem  13718  injresinj  13719  fldiv4p1lem1div2  13767  fldiv4lem1div2  13769  modfzo0difsn  13878  ssnn0fi  13920  fsuppmapnn0fiubex  13927  m1expcl2  14020  m1expeven  14044  zzlesq  14141  sq01  14160  expnngt1  14176  nn0opthi  14205  facp1  14213  faclbnd3  14227  faclbnd4lem1  14228  faclbnd4lem3  14230  bcn1  14248  hashnemnf  14279  hashv01gt1  14280  hashneq0  14299  hashrabrsn  14307  hashrabsn01  14308  hashrabsn1  14309  hashunx  14321  hashsnle1  14352  hashfzp1  14366  hash2pwpr  14411  hashge2el2difr  14416  swrdnd2  14591  pfxnd0  14624  repswswrd  14719  relexpsucl  14966  relexpsucr  14967  relexpcnv  14970  relexprelg  14973  relexpdmg  14977  relexprng  14981  relexpfld  14984  relexpaddg  14988  sumz  15657  arisum  15795  arisum2  15796  pwdif  15803  ntrivcvg  15832  prod1  15879  fprodfac  15908  mod2eq1n2dvds  16286  mulsucdiv2z  16292  nn0o1gt2  16320  nno  16321  nn0o  16322  sumeven  16326  sumodd  16327  divalglem1  16333  divalglem6  16337  gcdaddmlem  16463  dfgcd2  16485  mulgcd  16487  lcmf  16572  lcmfunsnlem2lem2  16578  lcmfunsnlem2  16579  prm2orodd  16630  dfphi2  16713  nnnn0modprm0  16746  prm23lt5  16754  oddprmdvds  16843  4sqlem19  16903  ramz  16965  prmolefac  16986  prmgaplem7  16997  cshwshashlem1  17035  ressval3d  17185  firest  17364  xpsfeq  17496  funcres2c  17839  ex-chn2  18573  smndex1basss  18842  smndex1mgm  18844  smndex1mndlem  18846  mulgnn0gsum  19022  symgfix2  19357  pmtrprfval  19428  m1expaddsub  19439  psgnprfval  19462  gsumpr  19896  gsumzunsnd  19897  0ringnnzr  20470  frgpcyg  21540  cnmsgnsubg  21544  psgninv  21549  zrhpsgnelbas  21561  m2detleiblem1  22580  symgmatr01lem  22609  indiscld  23047  pnfnei  23176  mnfnei  23177  alexsubALTlem2  24004  alexsubALTlem3  24005  dscmet  24528  xrtgioo  24763  ishl2  25338  iunmbl2  25526  icombl  25533  ioombl  25534  recnprss  25873  recnperf  25874  dvexp2  25926  dvexp3  25950  dvne0f1  25985  plypf1  26185  taylfvallem1  26332  taylfval  26334  tayl0  26337  coseq0negpitopi  26480  logfac  26578  cxpexp  26645  pythag  26795  reasinsin  26874  harmonicbnd3  26986  lgslem4  27279  gausslemma2dlem0i  27343  lgsquadlem2  27360  2lgslem3  27383  2lgs  27386  2lgsoddprmlem3  27393  2sqnn0  27417  2sqnn  27418  ltsres  27642  nolesgn2o  27651  nogesgn1o  27653  nosep1o  27661  nosep2o  27662  noetalem2  27722  sltsun1  27796  sltsun2  27797  eln0s  28369  n0zs  28397  bdaypw2n0bndlem  28471  bdaypw2n0bnd  28472  lfgrnloop  29210  uhgr2edg  29293  usgredg4  29302  usgredg2v  29312  usgrexmplef  29344  nb3grprlem1  29465  uvtx01vtx  29482  wlk1walk  29724  upgriswlk  29726  pthdadjvtx  29813  upgrwlkdvdelem  29821  pthdlem2lem  29852  pthspthcyc  29888  2pthon3v  30028  clwwlkn  30113  clwwlkneq0  30116  eupth2lem3lem4  30318  konigsberg  30344  3vfriswmgrlem  30364  1to2vfriswmgr  30366  1to3vfriswmgr  30367  frgrregorufr0  30411  numclwlk1  30458  ex-pr  30517  shunssi  31456  cvmdi  32412  1neg1t1neg1  32828  iundisj2cnt  32890  fz1nnct  32892  xrge0iifiso  34113  esumpr2  34245  measiuns  34395  sxbrsigalem0  34449  bnj964  35119  subfacval3  35405  kur14lem7  35428  satfrnmapom  35586  gonar  35611  goalr  35613  mrsubcv  35726  nepss  35934  nnuni  35943  fz0n  35947  bccolsum  35955  dfon2lem7  36003  altopthsn  36177  elhf2  36391  nn0prpw  36539  dissym1  36637  ordcmp  36663  bj-currypeirce  36781  bj-jaoi1  36796  bj-jaoi2  36797  bj-ififc  36807  bj-andnotim  36813  bj-nfimexal  36861  bj-sbsb  37085  bj-elsn12g  37308  bj-ideqg1  37419  finxpreclem2  37645  wl-equsal1i  37799  tan2h  37863  poimirlem23  37894  poimirlem32  37903  itg2addnclem  37922  orfa1  38336  orfa2  38337  inex3  38589  inxpex  38590  mopickr  38622  disjlem14  39152  elpadd0  40185  aks6d1c2p2  42489  sbor2  42582  sn-0ne2  42776  sn-0lt1  42845  hbtlem5  43485  omabs2  43689  safesnsupfiss  43771  safesnsupfidom1o  43773  safesnsupfilb  43774  rp-fakeimass  43868  rp-isfinite6  43874  pr2cv  43904  iunrelexp0  44058  relexpss1d  44061  relexpmulg  44066  iunrelexpmin2  44068  relexp01min  44069  relexp0a  44072  relexpxpmin  44073  relexpaddss  44074  clsk1indlem3  44399  ssrecnpr  44664  seff  44665  sblpnf  44666  expgrowthi  44689  dvconstbi  44690  19.33-2  44738  ax6e2ndeq  44915  en3lpVD  45200  undif3VD  45237  ax6e2ndeqVD  45264  ax6e2ndeqALT  45286  iooinlbub  45861  elprneb  47389  euoreqb  47469  2reu3  47470  afvpcfv0  47506  afvfv0bi  47512  afvco2  47536  afv2orxorb  47588  afv2ndeffv0  47620  afv2fv0b  47626  fvmptrabdm  47653  2ltceilhalf  47688  ceilhalfnn  47696  minusmodnep2tmod  47713  iccpartltu  47785  iccpartgtl  47786  iccpartgt  47787  iccpartleu  47788  iccpartgel  47789  iccpartnel  47798  elsprel  47835  prsprel  47847  sprsymrelfolem2  47853  paireqne  47871  odz2prm2pw  47923  fmtnofac1  47930  fmtno4prmfac  47932  31prm  47957  lighneallem2  47966  lighneallem3  47967  lighneallem4b  47969  lighneallem4  47970  zeo2ALTV  48031  nn0o1gt2ALTV  48054  nn0oALTV  48056  stgoldbwt  48136  sbgoldbwt  48137  sbgoldbalt  48141  sbgoldbm  48144  sbgoldbo  48147  nnsum3primesle9  48154  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  wtgoldbnnsum4prm  48162  bgoldbnnsum3prm  48164  bgoldbtbndlem1  48165  bgoldbtbnd  48169  tgoldbach  48177  vopnbgrelself  48215  clnbgrgrim  48294  grtriproplem  48299  grtrif1o  48302  grtriclwlk3  48305  gpgedgvtx0  48421  gpgcubic  48439  gpg5nbgr3star  48441  gpgprismgr4cycllem3  48457  gpgprismgr4cycllem7  48461  gpgprismgr4cycllem10  48464  pgnbgreunbgrlem3  48478  pgnbgreunbgrlem6  48484  pgnbgreunbgr  48485  upgrwlkupwlk  48500  ztprmneprm  48707  islinindfis  48809  lindslinindsimp2lem5  48822  lindslinindsimp2  48823  lindsrng01  48828  elfzolborelfzop1  48879  flnn0div2ge  48893  blennn0elnn  48937  blen1b  48948  nnolog2flm1  48950  blengt1fldiv2p1  48953  0dig2pr01  48970  dignn0flhalf  48978  nn0sumshdiglemB  48980  nn0sumshdiglem1  48981  resum2sqorgt0  49069  rrx2xpref1o  49078  rrx2plord2  49082  itsclc0yqsol  49124  mosssn  49174  mo0sn  49175  mofsssn  49205  mofmo  49206  f1omo  49252  f1omoOLD  49253