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  1884  19.33b  1885  nfim1  2200  dfsb2  2491  mooran1  2548  eueq3  3682  sbcor  3804  sspss  4065  sspsstr  4071  elun  4116  ssun  4158  inss  4211  raaan2  4484  ifbi  4511  ifcomnan  4545  rabsnifsb  4686  tpprceq3  4768  tppreqb  4769  pwpw0  4777  sssn  4790  snsssn  4805  preq12b  4814  prnebg  4820  preq12nebg  4827  elpr2elpr  4833  prproe  4869  3elpr2eq  4870  unissint  4936  zfpair  5376  propeqop  5467  propssopi  5468  opthhausdorff  5477  opthhausdorff0  5478  iunopeqop  5481  relsnb  5765  iresn0n0  6025  sotri2  6102  sotri3  6103  somincom  6107  ordssun  6436  unizlim  6457  onxpdisj  6460  tpres  7175  sorpssuni  7708  ordeleqon  7758  ordunisuc  7807  orduninsuc  7819  tfinds  7836  limomss  7847  limom  7858  soxp  8108  ressuppssdif  8164  tfr2b  8364  omopthi  8625  domnsym  9067  brwdom  9520  cantnfvalf  9618  ttrclselem1  9678  djuss  9873  djuunxp  9874  eldju2ndl  9877  eldju2ndr  9878  djuun  9879  updjud  9887  iscard3  10046  cflim2  10216  sornom  10230  isfin5  10252  isfin6  10253  sdom2en01  10255  fin23lem29  10294  fin23lem30  10295  fin56  10346  fin67  10348  hsmexlem9  10378  axcc4dom  10394  axdc3lem2  10404  axdc3lem4  10406  brdom3  10481  winainflem  10646  r1tskina  10735  indpi  10860  ltxrlt  11244  nn0sub  12492  nn0n0n1ge2b  12511  nn0ge2m1nn  12512  xnn0xr  12520  xnn0nemnf  12526  elnn0z  12542  nn0lt10b  12596  nn0le2is012  12598  nn0ind-raph  12634  uzin  12833  indstr2  12886  nn0ledivnn  13066  xrnemnf  13077  xrnepnf  13078  mnfltxr  13087  xnn0n0n1ge2b  13092  xnn0ge0  13094  xnn0xaddcl  13195  xnn0lenn0nn0  13205  xnn0xadd0  13207  xmullem2  13225  rexmul  13231  xnn0xrge0  13467  elfzonlteqm1  13702  elfznelfzo  13733  injresinjlem  13748  injresinj  13749  fldiv4p1lem1div2  13797  fldiv4lem1div2  13799  modfzo0difsn  13908  ssnn0fi  13950  fsuppmapnn0fiubex  13957  m1expcl2  14050  m1expeven  14074  zzlesq  14171  sq01  14190  expnngt1  14206  nn0opthi  14235  facp1  14243  faclbnd3  14257  faclbnd4lem1  14258  faclbnd4lem3  14260  bcn1  14278  hashnemnf  14309  hashv01gt1  14310  hashneq0  14329  hashrabrsn  14337  hashrabsn01  14338  hashrabsn1  14339  hashunx  14351  hashsnle1  14382  hashfzp1  14396  hash2pwpr  14441  hashge2el2difr  14446  swrdnd2  14620  pfxnd0  14653  repswswrd  14749  relexpsucl  14997  relexpsucr  14998  relexpcnv  15001  relexprelg  15004  relexpdmg  15008  relexprng  15012  relexpfld  15015  relexpaddg  15019  sumz  15688  arisum  15826  arisum2  15827  pwdif  15834  ntrivcvg  15863  prod1  15910  fprodfac  15939  mod2eq1n2dvds  16317  mulsucdiv2z  16323  nn0o1gt2  16351  nno  16352  nn0o  16353  sumeven  16357  sumodd  16358  divalglem1  16364  divalglem6  16368  gcdaddmlem  16494  dfgcd2  16516  mulgcd  16518  lcmf  16603  lcmfunsnlem2lem2  16609  lcmfunsnlem2  16610  prm2orodd  16661  dfphi2  16744  nnnn0modprm0  16777  prm23lt5  16785  oddprmdvds  16874  4sqlem19  16934  ramz  16996  prmolefac  17017  prmgaplem7  17028  cshwshashlem1  17066  ressval3d  17216  firest  17395  xpsfeq  17526  funcres2c  17865  smndex1basss  18832  smndex1mgm  18834  smndex1mndlem  18836  mulgnn0gsum  19012  symgfix2  19346  pmtrprfval  19417  m1expaddsub  19428  psgnprfval  19451  gsumpr  19885  gsumzunsnd  19886  0ringnnzr  20434  frgpcyg  21483  cnmsgnsubg  21486  psgninv  21491  zrhpsgnelbas  21503  m2detleiblem1  22511  symgmatr01lem  22540  indiscld  22978  pnfnei  23107  mnfnei  23108  alexsubALTlem2  23935  alexsubALTlem3  23936  dscmet  24460  xrtgioo  24695  ishl2  25270  iunmbl2  25458  icombl  25465  ioombl  25466  recnprss  25805  recnperf  25806  dvexp2  25858  dvexp3  25882  dvne0f1  25917  plypf1  26117  taylfvallem1  26264  taylfval  26266  tayl0  26269  coseq0negpitopi  26412  logfac  26510  cxpexp  26577  pythag  26727  reasinsin  26806  harmonicbnd3  26918  lgslem4  27211  gausslemma2dlem0i  27275  lgsquadlem2  27292  2lgslem3  27315  2lgs  27318  2lgsoddprmlem3  27325  2sqnn0  27349  2sqnn  27350  sltres  27574  nolesgn2o  27583  nogesgn1o  27585  nosep1o  27593  nosep2o  27594  noetalem2  27654  ssltun1  27720  ssltun2  27721  eln0s  28251  n0zs  28277  lfgrnloop  29052  uhgr2edg  29135  usgredg4  29144  usgredg2v  29154  usgrexmplef  29186  nb3grprlem1  29307  uvtx01vtx  29324  wlk1walk  29567  upgriswlk  29569  pthdadjvtx  29658  upgrwlkdvdelem  29666  pthdlem2lem  29697  pthspthcyc  29733  2pthon3v  29873  clwwlkn  29955  clwwlkneq0  29958  eupth2lem3lem4  30160  konigsberg  30186  3vfriswmgrlem  30206  1to2vfriswmgr  30208  1to3vfriswmgr  30209  frgrregorufr0  30253  numclwlk1  30300  ex-pr  30359  shunssi  31297  cvmdi  32253  1neg1t1neg1  32661  iundisj2cnt  32722  fz1nnct  32726  xrge0iifiso  33925  esumpr2  34057  measiuns  34207  sxbrsigalem0  34262  bnj964  34933  subfacval3  35176  kur14lem7  35199  satfrnmapom  35357  gonar  35382  goalr  35384  mrsubcv  35497  nepss  35705  nnuni  35714  fz0n  35718  bccolsum  35726  dfon2lem7  35777  altopthsn  35949  elhf2  36163  nn0prpw  36311  dissym1  36409  ordcmp  36435  bj-currypeirce  36545  bj-jaoi1  36559  bj-jaoi2  36560  bj-ififc  36570  bj-andnotim  36576  bj-nfimexal  36614  bj-sbsb  36825  bj-elsn12g  37048  bj-ideqg1  37152  finxpreclem2  37378  wl-equsal1i  37532  tan2h  37606  poimirlem23  37637  poimirlem32  37646  itg2addnclem  37665  orfa1  38079  orfa2  38080  inex3  38320  inxpex  38321  mopickr  38345  disjlem14  38790  elpadd0  39803  aks6d1c2p2  42107  sbor2  42200  sn-0ne2  42394  sn-0lt1  42463  hbtlem5  43117  omabs2  43321  safesnsupfiss  43404  safesnsupfidom1o  43406  safesnsupfilb  43407  rp-fakeimass  43501  rp-isfinite6  43507  pr2cv  43537  iunrelexp0  43691  relexpss1d  43694  relexpmulg  43699  iunrelexpmin2  43701  relexp01min  43702  relexp0a  43705  relexpxpmin  43706  relexpaddss  43707  clsk1indlem3  44032  ssrecnpr  44297  seff  44298  sblpnf  44299  expgrowthi  44322  dvconstbi  44323  19.33-2  44371  ax6e2ndeq  44549  en3lpVD  44834  undif3VD  44871  ax6e2ndeqVD  44898  ax6e2ndeqALT  44920  iooinlbub  45499  elprneb  47030  euoreqb  47110  2reu3  47111  afvpcfv0  47147  afvfv0bi  47153  afvco2  47177  afv2orxorb  47229  afv2ndeffv0  47261  afv2fv0b  47267  fvmptrabdm  47294  2ltceilhalf  47329  ceilhalfnn  47337  minusmodnep2tmod  47354  iccpartltu  47426  iccpartgtl  47427  iccpartgt  47428  iccpartleu  47429  iccpartgel  47430  iccpartnel  47439  elsprel  47476  prsprel  47488  sprsymrelfolem2  47494  paireqne  47512  odz2prm2pw  47564  fmtnofac1  47571  fmtno4prmfac  47573  31prm  47598  lighneallem2  47607  lighneallem3  47608  lighneallem4b  47610  lighneallem4  47611  zeo2ALTV  47672  nn0o1gt2ALTV  47695  nn0oALTV  47697  stgoldbwt  47777  sbgoldbwt  47778  sbgoldbalt  47782  sbgoldbm  47785  sbgoldbo  47788  nnsum3primesle9  47795  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  bgoldbtbndlem1  47806  bgoldbtbnd  47810  tgoldbach  47818  vopnbgrelself  47855  clnbgrgrim  47934  grtriproplem  47938  grtrif1o  47941  grtriclwlk3  47944  gpgedgvtx0  48052  gpgcubic  48070  gpg5nbgr3star  48072  gpgprismgr4cycllem3  48087  gpgprismgr4cycllem7  48091  gpgprismgr4cycllem10  48094  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114  pgnbgreunbgr  48115  upgrwlkupwlk  48128  ztprmneprm  48335  islinindfis  48438  lindslinindsimp2lem5  48451  lindslinindsimp2  48452  lindsrng01  48457  elfzolborelfzop1  48508  flnn0div2ge  48522  blennn0elnn  48566  blen1b  48577  nnolog2flm1  48579  blengt1fldiv2p1  48582  0dig2pr01  48599  dignn0flhalf  48607  nn0sumshdiglemB  48609  nn0sumshdiglem1  48610  resum2sqorgt0  48698  rrx2xpref1o  48707  rrx2plord2  48711  itsclc0yqsol  48753  mosssn  48803  mo0sn  48804  mofsssn  48834  mofmo  48835  f1omo  48881  f1omoOLD  48882