Theorem jaoi 855

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 849	. . 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 845

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 206  df-or 846

This theorem is referenced by:  jao1i  856  jaod  857  pm1.4  867  pm3.2ni  878  pm1.2  901  pm2.4  904  pm2.41  905  orim12i  906  pm1.5  917  pm2.42  940  jaoa  953  jaoian  954  pm4.44  994  andi  1005  ecase3  1029  cases2ALT  1046  consensus  1050  jaoi3  1058  1fpid3  1079  19.33  1879  19.33b  1880  nfim1  2187  dfsb2  2487  mooran1  2544  eueq3  3706  sbcor  3830  sspss  4097  sspsstr  4103  elun  4147  ssun  4189  inss  4239  raaan2  4526  ifbi  4552  ifcomnan  4586  elpr2OLD  4657  rabsnifsb  4729  tpprceq3  4810  tppreqb  4811  pwpw0  4819  sssn  4832  snsssn  4845  preq12b  4854  prnebg  4859  preq12nebg  4866  elpr2elpr  4872  prproe  4908  3elpr2eq  4909  unissint  4977  zfpair  5423  propeqop  5511  propssopi  5512  opthhausdorff  5521  opthhausdorff0  5522  iunopeqop  5525  relsnb  5806  iresn0n0  6060  sotri2  6138  sotri3  6139  somincom  6143  ordssun  6474  unizlim  6495  onxpdisj  6498  tpres  7217  sorpssuni  7741  ordeleqon  7788  ordunisuc  7839  orduninsuc  7851  tfinds  7868  limomss  7879  limom  7890  soxp  8138  ressuppssdif  8194  tfr2b  8421  omopthi  8686  domnsym  9128  brwdom  9596  cantnfvalf  9694  ttrclselem1  9754  djuss  9949  djuunxp  9950  eldju2ndl  9953  eldju2ndr  9954  djuun  9955  updjud  9963  iscard3  10122  cflim2  10292  sornom  10306  isfin5  10328  isfin6  10329  sdom2en01  10331  fin23lem29  10370  fin23lem30  10371  fin56  10422  fin67  10424  hsmexlem9  10454  axcc4dom  10470  axdc3lem2  10480  axdc3lem4  10482  brdom3  10557  winainflem  10722  r1tskina  10811  indpi  10936  ltxrlt  11320  nn0sub  12558  nn0n0n1ge2b  12576  nn0ge2m1nn  12577  xnn0xr  12585  xnn0nemnf  12591  elnn0z  12607  nn0lt10b  12660  nn0le2is012  12662  nn0ind-raph  12698  uzin  12898  indstr2  12947  nn0ledivnn  13125  xrnemnf  13135  xrnepnf  13136  mnfltxr  13145  xnn0n0n1ge2b  13149  xnn0ge0  13151  xnn0xaddcl  13252  xnn0lenn0nn0  13262  xnn0xadd0  13264  xmullem2  13282  rexmul  13288  xnn0xrge0  13521  elfzonlteqm1  13746  elfznelfzo  13775  injresinjlem  13790  injresinj  13791  fldiv4p1lem1div2  13838  fldiv4lem1div2  13840  modfzo0difsn  13946  ssnn0fi  13988  fsuppmapnn0fiubex  13995  m1expcl2  14088  m1expeven  14112  zzlesq  14207  sq01  14225  expnngt1  14241  nn0opthi  14267  facp1  14275  faclbnd3  14289  faclbnd4lem1  14290  faclbnd4lem3  14292  bcn1  14310  hashnemnf  14341  hashv01gt1  14342  hashneq0  14361  hashrabrsn  14369  hashrabsn01  14370  hashrabsn1  14371  hashunx  14383  hashsnle1  14414  hashfzp1  14428  hash2pwpr  14475  hashge2el2difr  14480  swrdnd2  14643  pfxnd0  14676  repswswrd  14772  relexpsucl  15016  relexpsucr  15017  relexpcnv  15020  relexprelg  15023  relexpdmg  15027  relexprng  15031  relexpfld  15034  relexpaddg  15038  sumz  15706  arisum  15844  arisum2  15845  pwdif  15852  ntrivcvg  15881  prod1  15926  fprodfac  15955  mod2eq1n2dvds  16329  mulsucdiv2z  16335  nn0o1gt2  16363  nno  16364  nn0o  16365  sumeven  16369  sumodd  16370  divalglem1  16376  divalglem6  16380  gcdaddmlem  16504  dfgcd2  16527  mulgcd  16529  lcmf  16609  lcmfunsnlem2lem2  16615  lcmfunsnlem2  16616  prm2orodd  16667  dfphi2  16748  nnnn0modprm0  16780  prm23lt5  16788  oddprmdvds  16877  4sqlem19  16937  ramz  16999  prmolefac  17020  prmgaplem7  17031  cshwshashlem1  17070  ressval3d  17232  ressval3dOLD  17233  firest  17419  xpsfeq  17550  funcres2c  17895  smndex1basss  18862  smndex1mgm  18864  smndex1mndlem  18866  mulgnn0gsum  19040  symgfix2  19376  pmtrprfval  19447  m1expaddsub  19458  psgnprfval  19481  gsumpr  19915  gsumzunsnd  19916  0ringnnzr  20467  sralemOLD  21067  frgpcyg  21512  cnmsgnsubg  21514  psgninv  21519  zrhpsgnelbas  21531  m2detleiblem1  22544  symgmatr01lem  22573  indiscld  23013  pnfnei  23142  mnfnei  23143  alexsubALTlem2  23970  alexsubALTlem3  23971  dscmet  24499  xrtgioo  24740  ishl2  25316  iunmbl2  25504  icombl  25511  ioombl  25512  recnprss  25851  recnperf  25852  dvexp2  25904  dvexp3  25928  dvne0f1  25963  plypf1  26164  taylfvallem1  26309  taylfval  26311  tayl0  26314  coseq0negpitopi  26456  logfac  26553  cxpexp  26620  pythag  26767  reasinsin  26846  harmonicbnd3  26958  lgslem4  27251  gausslemma2dlem0i  27315  lgsquadlem2  27332  2lgslem3  27355  2lgs  27358  2lgsoddprmlem3  27365  2sqnn0  27389  2sqnn  27390  sltres  27613  nolesgn2o  27622  nogesgn1o  27624  nosep1o  27632  nosep2o  27633  noetalem2  27693  ssltun1  27759  ssltun2  27760  cchhllemOLD  28716  lfgrnloop  28956  uhgr2edg  29039  usgredg4  29048  usgredg2v  29058  usgrexmplef  29090  nb3grprlem1  29211  uvtx01vtx  29228  wlk1walk  29471  upgriswlk  29473  pthdadjvtx  29562  upgrwlkdvdelem  29568  pthdlem2lem  29599  2pthon3v  29772  clwwlkn  29854  clwwlkneq0  29857  eupth2lem3lem4  30059  konigsberg  30085  3vfriswmgrlem  30105  1to2vfriswmgr  30107  1to3vfriswmgr  30108  frgrregorufr0  30152  numclwlk1  30199  ex-pr  30258  shunssi  31196  cvmdi  32152  1neg1t1neg1  32537  iundisj2cnt  32585  fz1nnct  32589  xrge0iifiso  33541  esumpr2  33691  measiuns  33841  sxbrsigalem0  33896  bnj964  34579  subfacval3  34804  kur14lem7  34827  satfrnmapom  34985  gonar  35010  goalr  35012  mrsubcv  35125  nepss  35317  nnuni  35326  fz0n  35330  bccolsum  35338  dfon2lem7  35390  altopthsn  35562  elhf2  35776  nn0prpw  35812  dissym1  35910  ordcmp  35936  bj-currypeirce  36037  bj-jaoi1  36052  bj-jaoi2  36053  bj-ififc  36063  bj-andnotim  36070  bj-nfimexal  36107  bj-sbsb  36319  bj-elsn12g  36544  bj-ideqg1  36648  finxpreclem2  36874  wl-equsal1i  37016  tan2h  37090  poimirlem23  37121  poimirlem32  37130  itg2addnclem  37149  orfa1  37563  orfa2  37564  imaexALTV  37806  inex3  37814  inxpex  37815  mopickr  37839  disjlem14  38274  elpadd0  39286  aks6d1c2p2  41594  sbor2  41703  sn-0ne2  41964  sn-0lt1  42020  hbtlem5  42555  omabs2  42764  safesnsupfiss  42848  safesnsupfidom1o  42850  safesnsupfilb  42851  rp-fakeimass  42945  rp-isfinite6  42951  pr2cv  42981  iunrelexp0  43135  relexpss1d  43138  relexpmulg  43143  iunrelexpmin2  43145  relexp01min  43146  relexp0a  43149  relexpxpmin  43150  relexpaddss  43151  clsk1indlem3  43476  ssrecnpr  43748  seff  43749  sblpnf  43750  expgrowthi  43773  dvconstbi  43774  19.33-2  43822  ax6e2ndeq  44001  en3lpVD  44287  undif3VD  44324  ax6e2ndeqVD  44351  ax6e2ndeqALT  44373  iooinlbub  44888  elprneb  46413  euoreqb  46491  2reu3  46492  afvpcfv0  46528  afvfv0bi  46534  afvco2  46558  afv2orxorb  46610  afv2ndeffv0  46642  afv2fv0b  46648  fvmptrabdm  46675  iccpartltu  46767  iccpartgtl  46768  iccpartgt  46769  iccpartleu  46770  iccpartgel  46771  iccpartnel  46780  elsprel  46817  prsprel  46829  sprsymrelfolem2  46835  paireqne  46853  odz2prm2pw  46905  fmtnofac1  46912  fmtno4prmfac  46914  31prm  46939  lighneallem2  46948  lighneallem3  46949  lighneallem4b  46951  lighneallem4  46952  zeo2ALTV  47013  nn0o1gt2ALTV  47036  nn0oALTV  47038  stgoldbwt  47118  sbgoldbwt  47119  sbgoldbalt  47123  sbgoldbm  47126  sbgoldbo  47129  nnsum3primesle9  47136  nnsum4primeseven  47142  nnsum4primesevenALTV  47143  wtgoldbnnsum4prm  47144  bgoldbnnsum3prm  47146  bgoldbtbndlem1  47147  bgoldbtbnd  47151  tgoldbach  47159  vopnbgrelself  47192  upgrwlkupwlk  47253  ztprmneprm  47462  islinindfis  47568  lindslinindsimp2lem5  47581  lindslinindsimp2  47582  lindsrng01  47587  elfzolborelfzop1  47638  flnn0div2ge  47657  blennn0elnn  47701  blen1b  47712  nnolog2flm1  47714  blengt1fldiv2p1  47717  0dig2pr01  47734  dignn0flhalf  47742  nn0sumshdiglemB  47744  nn0sumshdiglem1  47745  resum2sqorgt0  47833  rrx2xpref1o  47842  rrx2plord2  47846  itsclc0yqsol  47888  mosssn  47936  mo0sn  47937  mofsssn  47949  mofmo  47950  f1omo  47964