Theorem jaoi 857

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 851	. . 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 847

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 848

This theorem is referenced by:  jao1i  858  jaod  859  pm1.4  869  pm3.2ni  880  pm1.2  903  pm2.4  906  pm2.41  907  orim12i  908  pm1.5  919  pm2.42  944  jaoa  957  jaoian  958  pm4.44  998  andi  1009  ecase3  1032  cases2ALT  1048  consensus  1052  jaoi3  1060  1fpid3  1081  19.33  1885  19.33b  1886  nfim1  2204  dfsb2  2495  mooran1  2553  eueq3  3667  sbcor  3789  sspss  4052  sspsstr  4058  elun  4103  ssun  4145  inss  4198  raaan2  4473  ifbi  4500  ifcomnan  4534  rabsnifsb  4677  tpprceq3  4758  tppreqb  4759  pwpw0  4767  sssn  4780  snsssn  4795  preq12b  4804  prnebg  4810  preq12nebg  4817  elpr2elpr  4823  prproe  4859  3elpr2eq  4860  unissint  4925  zfpair  5364  propeqop  5453  propssopi  5454  opthhausdorff  5463  opthhausdorff0  5464  iunopeqop  5467  relsnb  5749  iresn0n0  6011  sotri2  6084  sotri3  6085  somincom  6089  ordssun  6419  unizlim  6439  onxpdisj  6442  tpres  7145  sorpssuni  7675  ordeleqon  7725  ordunisuc  7772  orduninsuc  7783  tfinds  7800  limomss  7811  limom  7822  soxp  8069  ressuppssdif  8125  tfr2b  8325  omopthi  8587  domnsym  9029  ordfin  9138  brwdom  9470  cantnfvalf  9572  ttrclselem1  9632  djuss  9830  djuunxp  9831  eldju2ndl  9834  eldju2ndr  9835  djuun  9836  updjud  9844  iscard3  10001  cflim2  10171  sornom  10185  isfin5  10207  isfin6  10208  sdom2en01  10210  fin23lem29  10249  fin23lem30  10250  fin56  10301  fin67  10303  hsmexlem9  10333  axcc4dom  10349  axdc3lem2  10359  axdc3lem4  10361  brdom3  10436  winainflem  10602  r1tskina  10691  indpi  10816  ltxrlt  11201  nn0sub  12449  nn0n0n1ge2b  12468  nn0ge2m1nn  12469  xnn0xr  12477  xnn0nemnf  12483  elnn0z  12499  nn0lt10b  12552  nn0le2is012  12554  nn0ind-raph  12590  uzin  12785  indstr2  12838  nn0ledivnn  13018  xrnemnf  13029  xrnepnf  13030  mnfltxr  13039  xnn0n0n1ge2b  13044  xnn0ge0  13046  xnn0xaddcl  13148  xnn0lenn0nn0  13158  xnn0xadd0  13160  xmullem2  13178  rexmul  13184  xnn0xrge0  13420  elfzonlteqm1  13655  elfznelfzo  13687  injresinjlem  13704  injresinj  13705  fldiv4p1lem1div2  13753  fldiv4lem1div2  13755  modfzo0difsn  13864  ssnn0fi  13906  fsuppmapnn0fiubex  13913  m1expcl2  14006  m1expeven  14030  zzlesq  14127  sq01  14146  expnngt1  14162  nn0opthi  14191  facp1  14199  faclbnd3  14213  faclbnd4lem1  14214  faclbnd4lem3  14216  bcn1  14234  hashnemnf  14265  hashv01gt1  14266  hashneq0  14285  hashrabrsn  14293  hashrabsn01  14294  hashrabsn1  14295  hashunx  14307  hashsnle1  14338  hashfzp1  14352  hash2pwpr  14397  hashge2el2difr  14402  swrdnd2  14577  pfxnd0  14610  repswswrd  14705  relexpsucl  14952  relexpsucr  14953  relexpcnv  14956  relexprelg  14959  relexpdmg  14963  relexprng  14967  relexpfld  14970  relexpaddg  14974  sumz  15643  arisum  15781  arisum2  15782  pwdif  15789  ntrivcvg  15818  prod1  15865  fprodfac  15894  mod2eq1n2dvds  16272  mulsucdiv2z  16278  nn0o1gt2  16306  nno  16307  nn0o  16308  sumeven  16312  sumodd  16313  divalglem1  16319  divalglem6  16323  gcdaddmlem  16449  dfgcd2  16471  mulgcd  16473  lcmf  16558  lcmfunsnlem2lem2  16564  lcmfunsnlem2  16565  prm2orodd  16616  dfphi2  16699  nnnn0modprm0  16732  prm23lt5  16740  oddprmdvds  16829  4sqlem19  16889  ramz  16951  prmolefac  16972  prmgaplem7  16983  cshwshashlem1  17021  ressval3d  17171  firest  17350  xpsfeq  17482  funcres2c  17825  ex-chn2  18559  smndex1basss  18828  smndex1mgm  18830  smndex1mndlem  18832  mulgnn0gsum  19008  symgfix2  19343  pmtrprfval  19414  m1expaddsub  19425  psgnprfval  19448  gsumpr  19882  gsumzunsnd  19883  0ringnnzr  20456  frgpcyg  21526  cnmsgnsubg  21530  psgninv  21535  zrhpsgnelbas  21547  m2detleiblem1  22566  symgmatr01lem  22595  indiscld  23033  pnfnei  23162  mnfnei  23163  alexsubALTlem2  23990  alexsubALTlem3  23991  dscmet  24514  xrtgioo  24749  ishl2  25324  iunmbl2  25512  icombl  25519  ioombl  25520  recnprss  25859  recnperf  25860  dvexp2  25912  dvexp3  25936  dvne0f1  25971  plypf1  26171  taylfvallem1  26318  taylfval  26320  tayl0  26323  coseq0negpitopi  26466  logfac  26564  cxpexp  26631  pythag  26781  reasinsin  26860  harmonicbnd3  26972  lgslem4  27265  gausslemma2dlem0i  27329  lgsquadlem2  27346  2lgslem3  27369  2lgs  27372  2lgsoddprmlem3  27379  2sqnn0  27403  2sqnn  27404  sltres  27628  nolesgn2o  27637  nogesgn1o  27639  nosep1o  27647  nosep2o  27648  noetalem2  27708  ssltun1  27776  ssltun2  27777  eln0s  28320  n0zs  28347  bdaypw2n0s  28420  lfgrnloop  29147  uhgr2edg  29230  usgredg4  29239  usgredg2v  29249  usgrexmplef  29281  nb3grprlem1  29402  uvtx01vtx  29419  wlk1walk  29661  upgriswlk  29663  pthdadjvtx  29750  upgrwlkdvdelem  29758  pthdlem2lem  29789  pthspthcyc  29825  2pthon3v  29965  clwwlkn  30050  clwwlkneq0  30053  eupth2lem3lem4  30255  konigsberg  30281  3vfriswmgrlem  30301  1to2vfriswmgr  30303  1to3vfriswmgr  30304  frgrregorufr0  30348  numclwlk1  30395  ex-pr  30454  shunssi  31392  cvmdi  32348  1neg1t1neg1  32766  iundisj2cnt  32828  fz1nnct  32830  xrge0iifiso  34041  esumpr2  34173  measiuns  34323  sxbrsigalem0  34377  bnj964  35048  subfacval3  35332  kur14lem7  35355  satfrnmapom  35513  gonar  35538  goalr  35540  mrsubcv  35653  nepss  35861  nnuni  35870  fz0n  35874  bccolsum  35882  dfon2lem7  35930  altopthsn  36104  elhf2  36318  nn0prpw  36466  dissym1  36564  ordcmp  36590  bj-currypeirce  36700  bj-jaoi1  36714  bj-jaoi2  36715  bj-ififc  36725  bj-andnotim  36731  bj-nfimexal  36769  bj-sbsb  36981  bj-elsn12g  37204  bj-ideqg1  37308  finxpreclem2  37534  wl-equsal1i  37688  tan2h  37752  poimirlem23  37783  poimirlem32  37792  itg2addnclem  37811  orfa1  38225  orfa2  38226  inex3  38470  inxpex  38471  mopickr  38495  disjlem14  38996  elpadd0  40008  aks6d1c2p2  42312  sbor2  42405  sn-0ne2  42603  sn-0lt1  42672  hbtlem5  43312  omabs2  43516  safesnsupfiss  43598  safesnsupfidom1o  43600  safesnsupfilb  43601  rp-fakeimass  43695  rp-isfinite6  43701  pr2cv  43731  iunrelexp0  43885  relexpss1d  43888  relexpmulg  43893  iunrelexpmin2  43895  relexp01min  43896  relexp0a  43899  relexpxpmin  43900  relexpaddss  43901  clsk1indlem3  44226  ssrecnpr  44491  seff  44492  sblpnf  44493  expgrowthi  44516  dvconstbi  44517  19.33-2  44565  ax6e2ndeq  44742  en3lpVD  45027  undif3VD  45064  ax6e2ndeqVD  45091  ax6e2ndeqALT  45113  iooinlbub  45689  elprneb  47217  euoreqb  47297  2reu3  47298  afvpcfv0  47334  afvfv0bi  47340  afvco2  47364  afv2orxorb  47416  afv2ndeffv0  47448  afv2fv0b  47454  fvmptrabdm  47481  2ltceilhalf  47516  ceilhalfnn  47524  minusmodnep2tmod  47541  iccpartltu  47613  iccpartgtl  47614  iccpartgt  47615  iccpartleu  47616  iccpartgel  47617  iccpartnel  47626  elsprel  47663  prsprel  47675  sprsymrelfolem2  47681  paireqne  47699  odz2prm2pw  47751  fmtnofac1  47758  fmtno4prmfac  47760  31prm  47785  lighneallem2  47794  lighneallem3  47795  lighneallem4b  47797  lighneallem4  47798  zeo2ALTV  47859  nn0o1gt2ALTV  47882  nn0oALTV  47884  stgoldbwt  47964  sbgoldbwt  47965  sbgoldbalt  47969  sbgoldbm  47972  sbgoldbo  47975  nnsum3primesle9  47982  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  wtgoldbnnsum4prm  47990  bgoldbnnsum3prm  47992  bgoldbtbndlem1  47993  bgoldbtbnd  47997  tgoldbach  48005  vopnbgrelself  48043  clnbgrgrim  48122  grtriproplem  48127  grtrif1o  48130  grtriclwlk3  48133  gpgedgvtx0  48249  gpgcubic  48267  gpg5nbgr3star  48269  gpgprismgr4cycllem3  48285  gpgprismgr4cycllem7  48289  gpgprismgr4cycllem10  48292  pgnbgreunbgrlem3  48306  pgnbgreunbgrlem6  48312  pgnbgreunbgr  48313  upgrwlkupwlk  48328  ztprmneprm  48535  islinindfis  48637  lindslinindsimp2lem5  48650  lindslinindsimp2  48651  lindsrng01  48656  elfzolborelfzop1  48707  flnn0div2ge  48721  blennn0elnn  48765  blen1b  48776  nnolog2flm1  48778  blengt1fldiv2p1  48781  0dig2pr01  48798  dignn0flhalf  48806  nn0sumshdiglemB  48808  nn0sumshdiglem1  48809  resum2sqorgt0  48897  rrx2xpref1o  48906  rrx2plord2  48910  itsclc0yqsol  48952  mosssn  49002  mo0sn  49003  mofsssn  49033  mofmo  49034  f1omo  49080  f1omoOLD  49081