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  3679  sbcor  3801  sspss  4061  sspsstr  4067  elun  4112  ssun  4154  inss  4207  raaan2  4480  ifbi  4507  ifcomnan  4541  rabsnifsb  4682  tpprceq3  4764  tppreqb  4765  pwpw0  4773  sssn  4786  snsssn  4801  preq12b  4810  prnebg  4816  preq12nebg  4823  elpr2elpr  4829  prproe  4865  3elpr2eq  4866  unissint  4932  zfpair  5371  propeqop  5462  propssopi  5463  opthhausdorff  5472  opthhausdorff0  5473  iunopeqop  5476  relsnb  5756  iresn0n0  6014  sotri2  6090  sotri3  6091  somincom  6095  ordssun  6424  unizlim  6445  onxpdisj  6448  tpres  7157  sorpssuni  7688  ordeleqon  7738  ordunisuc  7787  orduninsuc  7799  tfinds  7816  limomss  7827  limom  7838  soxp  8085  ressuppssdif  8141  tfr2b  8341  omopthi  8602  domnsym  9044  brwdom  9496  cantnfvalf  9594  ttrclselem1  9654  djuss  9849  djuunxp  9850  eldju2ndl  9853  eldju2ndr  9854  djuun  9855  updjud  9863  iscard3  10022  cflim2  10192  sornom  10206  isfin5  10228  isfin6  10229  sdom2en01  10231  fin23lem29  10270  fin23lem30  10271  fin56  10322  fin67  10324  hsmexlem9  10354  axcc4dom  10370  axdc3lem2  10380  axdc3lem4  10382  brdom3  10457  winainflem  10622  r1tskina  10711  indpi  10836  ltxrlt  11220  nn0sub  12468  nn0n0n1ge2b  12487  nn0ge2m1nn  12488  xnn0xr  12496  xnn0nemnf  12502  elnn0z  12518  nn0lt10b  12572  nn0le2is012  12574  nn0ind-raph  12610  uzin  12809  indstr2  12862  nn0ledivnn  13042  xrnemnf  13053  xrnepnf  13054  mnfltxr  13063  xnn0n0n1ge2b  13068  xnn0ge0  13070  xnn0xaddcl  13171  xnn0lenn0nn0  13181  xnn0xadd0  13183  xmullem2  13201  rexmul  13207  xnn0xrge0  13443  elfzonlteqm1  13678  elfznelfzo  13709  injresinjlem  13724  injresinj  13725  fldiv4p1lem1div2  13773  fldiv4lem1div2  13775  modfzo0difsn  13884  ssnn0fi  13926  fsuppmapnn0fiubex  13933  m1expcl2  14026  m1expeven  14050  zzlesq  14147  sq01  14166  expnngt1  14182  nn0opthi  14211  facp1  14219  faclbnd3  14233  faclbnd4lem1  14234  faclbnd4lem3  14236  bcn1  14254  hashnemnf  14285  hashv01gt1  14286  hashneq0  14305  hashrabrsn  14313  hashrabsn01  14314  hashrabsn1  14315  hashunx  14327  hashsnle1  14358  hashfzp1  14372  hash2pwpr  14417  hashge2el2difr  14422  swrdnd2  14596  pfxnd0  14629  repswswrd  14725  relexpsucl  14973  relexpsucr  14974  relexpcnv  14977  relexprelg  14980  relexpdmg  14984  relexprng  14988  relexpfld  14991  relexpaddg  14995  sumz  15664  arisum  15802  arisum2  15803  pwdif  15810  ntrivcvg  15839  prod1  15886  fprodfac  15915  mod2eq1n2dvds  16293  mulsucdiv2z  16299  nn0o1gt2  16327  nno  16328  nn0o  16329  sumeven  16333  sumodd  16334  divalglem1  16340  divalglem6  16344  gcdaddmlem  16470  dfgcd2  16492  mulgcd  16494  lcmf  16579  lcmfunsnlem2lem2  16585  lcmfunsnlem2  16586  prm2orodd  16637  dfphi2  16720  nnnn0modprm0  16753  prm23lt5  16761  oddprmdvds  16850  4sqlem19  16910  ramz  16972  prmolefac  16993  prmgaplem7  17004  cshwshashlem1  17042  ressval3d  17192  firest  17371  xpsfeq  17502  funcres2c  17845  smndex1basss  18814  smndex1mgm  18816  smndex1mndlem  18818  mulgnn0gsum  18994  symgfix2  19330  pmtrprfval  19401  m1expaddsub  19412  psgnprfval  19435  gsumpr  19869  gsumzunsnd  19870  0ringnnzr  20445  frgpcyg  21515  cnmsgnsubg  21519  psgninv  21524  zrhpsgnelbas  21536  m2detleiblem1  22544  symgmatr01lem  22573  indiscld  23011  pnfnei  23140  mnfnei  23141  alexsubALTlem2  23968  alexsubALTlem3  23969  dscmet  24493  xrtgioo  24728  ishl2  25303  iunmbl2  25491  icombl  25498  ioombl  25499  recnprss  25838  recnperf  25839  dvexp2  25891  dvexp3  25915  dvne0f1  25950  plypf1  26150  taylfvallem1  26297  taylfval  26299  tayl0  26302  coseq0negpitopi  26445  logfac  26543  cxpexp  26610  pythag  26760  reasinsin  26839  harmonicbnd3  26951  lgslem4  27244  gausslemma2dlem0i  27308  lgsquadlem2  27325  2lgslem3  27348  2lgs  27351  2lgsoddprmlem3  27358  2sqnn0  27382  2sqnn  27383  sltres  27607  nolesgn2o  27616  nogesgn1o  27618  nosep1o  27626  nosep2o  27627  noetalem2  27687  ssltun1  27754  ssltun2  27755  eln0s  28291  n0zs  28317  lfgrnloop  29105  uhgr2edg  29188  usgredg4  29197  usgredg2v  29207  usgrexmplef  29239  nb3grprlem1  29360  uvtx01vtx  29377  wlk1walk  29619  upgriswlk  29621  pthdadjvtx  29708  upgrwlkdvdelem  29716  pthdlem2lem  29747  pthspthcyc  29783  2pthon3v  29923  clwwlkn  30005  clwwlkneq0  30008  eupth2lem3lem4  30210  konigsberg  30236  3vfriswmgrlem  30256  1to2vfriswmgr  30258  1to3vfriswmgr  30259  frgrregorufr0  30303  numclwlk1  30350  ex-pr  30409  shunssi  31347  cvmdi  32303  1neg1t1neg1  32711  iundisj2cnt  32772  fz1nnct  32776  xrge0iifiso  33918  esumpr2  34050  measiuns  34200  sxbrsigalem0  34255  bnj964  34926  subfacval3  35169  kur14lem7  35192  satfrnmapom  35350  gonar  35375  goalr  35377  mrsubcv  35490  nepss  35698  nnuni  35707  fz0n  35711  bccolsum  35719  dfon2lem7  35770  altopthsn  35942  elhf2  36156  nn0prpw  36304  dissym1  36402  ordcmp  36428  bj-currypeirce  36538  bj-jaoi1  36552  bj-jaoi2  36553  bj-ififc  36563  bj-andnotim  36569  bj-nfimexal  36607  bj-sbsb  36818  bj-elsn12g  37041  bj-ideqg1  37145  finxpreclem2  37371  wl-equsal1i  37525  tan2h  37599  poimirlem23  37630  poimirlem32  37639  itg2addnclem  37658  orfa1  38072  orfa2  38073  inex3  38313  inxpex  38314  mopickr  38338  disjlem14  38783  elpadd0  39796  aks6d1c2p2  42100  sbor2  42193  sn-0ne2  42387  sn-0lt1  42456  hbtlem5  43110  omabs2  43314  safesnsupfiss  43397  safesnsupfidom1o  43399  safesnsupfilb  43400  rp-fakeimass  43494  rp-isfinite6  43500  pr2cv  43530  iunrelexp0  43684  relexpss1d  43687  relexpmulg  43692  iunrelexpmin2  43694  relexp01min  43695  relexp0a  43698  relexpxpmin  43699  relexpaddss  43700  clsk1indlem3  44025  ssrecnpr  44290  seff  44291  sblpnf  44292  expgrowthi  44315  dvconstbi  44316  19.33-2  44364  ax6e2ndeq  44542  en3lpVD  44827  undif3VD  44864  ax6e2ndeqVD  44891  ax6e2ndeqALT  44913  iooinlbub  45492  elprneb  47023  euoreqb  47103  2reu3  47104  afvpcfv0  47140  afvfv0bi  47146  afvco2  47170  afv2orxorb  47222  afv2ndeffv0  47254  afv2fv0b  47260  fvmptrabdm  47287  2ltceilhalf  47322  ceilhalfnn  47330  minusmodnep2tmod  47347  iccpartltu  47419  iccpartgtl  47420  iccpartgt  47421  iccpartleu  47422  iccpartgel  47423  iccpartnel  47432  elsprel  47469  prsprel  47481  sprsymrelfolem2  47487  paireqne  47505  odz2prm2pw  47557  fmtnofac1  47564  fmtno4prmfac  47566  31prm  47591  lighneallem2  47600  lighneallem3  47601  lighneallem4b  47603  lighneallem4  47604  zeo2ALTV  47665  nn0o1gt2ALTV  47688  nn0oALTV  47690  stgoldbwt  47770  sbgoldbwt  47771  sbgoldbalt  47775  sbgoldbm  47778  sbgoldbo  47781  nnsum3primesle9  47788  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  bgoldbtbndlem1  47799  bgoldbtbnd  47803  tgoldbach  47811  vopnbgrelself  47848  clnbgrgrim  47927  grtriproplem  47931  grtrif1o  47934  grtriclwlk3  47937  gpgedgvtx0  48045  gpgcubic  48063  gpg5nbgr3star  48065  gpgprismgr4cycllem3  48080  gpgprismgr4cycllem7  48084  gpgprismgr4cycllem10  48087  pgnbgreunbgrlem3  48101  pgnbgreunbgrlem6  48107  pgnbgreunbgr  48108  upgrwlkupwlk  48121  ztprmneprm  48328  islinindfis  48431  lindslinindsimp2lem5  48444  lindslinindsimp2  48445  lindsrng01  48450  elfzolborelfzop1  48501  flnn0div2ge  48515  blennn0elnn  48559  blen1b  48570  nnolog2flm1  48572  blengt1fldiv2p1  48575  0dig2pr01  48592  dignn0flhalf  48600  nn0sumshdiglemB  48602  nn0sumshdiglem1  48603  resum2sqorgt0  48691  rrx2xpref1o  48700  rrx2plord2  48704  itsclc0yqsol  48746  mosssn  48796  mo0sn  48797  mofsssn  48827  mofmo  48828  f1omo  48874  f1omoOLD  48875