Theorem jaoi 856

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 850	. . 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 846

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 847

This theorem is referenced by:  jao1i  857  jaod  858  pm1.4  868  pm3.2ni  879  pm1.2  902  pm2.4  905  pm2.41  906  orim12i  907  pm1.5  918  pm2.42  943  jaoa  956  jaoian  957  pm4.44  997  andi  1008  ecase3  1032  cases2ALT  1049  consensus  1053  jaoi3  1061  1fpid3  1082  19.33  1883  19.33b  1884  nfim1  2200  dfsb2  2501  mooran1  2558  eueq3  3733  sbcor  3858  sspss  4125  sspsstr  4131  elun  4176  ssun  4218  inss  4268  raaan2  4544  ifbi  4570  ifcomnan  4604  rabsnifsb  4747  tpprceq3  4829  tppreqb  4830  pwpw0  4838  sssn  4851  snsssn  4866  preq12b  4875  prnebg  4880  preq12nebg  4887  elpr2elpr  4893  prproe  4929  3elpr2eq  4930  unissint  4996  zfpair  5439  propeqop  5526  propssopi  5527  opthhausdorff  5536  opthhausdorff0  5537  iunopeqop  5540  relsnb  5826  iresn0n0  6083  sotri2  6161  sotri3  6162  somincom  6166  ordssun  6497  unizlim  6518  onxpdisj  6521  tpres  7238  sorpssuni  7767  ordeleqon  7817  ordunisuc  7868  orduninsuc  7880  tfinds  7897  limomss  7908  limom  7919  soxp  8170  ressuppssdif  8226  tfr2b  8452  omopthi  8717  domnsym  9165  brwdom  9636  cantnfvalf  9734  ttrclselem1  9794  djuss  9989  djuunxp  9990  eldju2ndl  9993  eldju2ndr  9994  djuun  9995  updjud  10003  iscard3  10162  cflim2  10332  sornom  10346  isfin5  10368  isfin6  10369  sdom2en01  10371  fin23lem29  10410  fin23lem30  10411  fin56  10462  fin67  10464  hsmexlem9  10494  axcc4dom  10510  axdc3lem2  10520  axdc3lem4  10522  brdom3  10597  winainflem  10762  r1tskina  10851  indpi  10976  ltxrlt  11360  nn0sub  12603  nn0n0n1ge2b  12621  nn0ge2m1nn  12622  xnn0xr  12630  xnn0nemnf  12636  elnn0z  12652  nn0lt10b  12705  nn0le2is012  12707  nn0ind-raph  12743  uzin  12943  indstr2  12992  nn0ledivnn  13170  xrnemnf  13180  xrnepnf  13181  mnfltxr  13190  xnn0n0n1ge2b  13194  xnn0ge0  13196  xnn0xaddcl  13297  xnn0lenn0nn0  13307  xnn0xadd0  13309  xmullem2  13327  rexmul  13333  xnn0xrge0  13566  elfzonlteqm1  13792  elfznelfzo  13822  injresinjlem  13837  injresinj  13838  fldiv4p1lem1div2  13886  fldiv4lem1div2  13888  modfzo0difsn  13994  ssnn0fi  14036  fsuppmapnn0fiubex  14043  m1expcl2  14136  m1expeven  14160  zzlesq  14255  sq01  14274  expnngt1  14290  nn0opthi  14319  facp1  14327  faclbnd3  14341  faclbnd4lem1  14342  faclbnd4lem3  14344  bcn1  14362  hashnemnf  14393  hashv01gt1  14394  hashneq0  14413  hashrabrsn  14421  hashrabsn01  14422  hashrabsn1  14423  hashunx  14435  hashsnle1  14466  hashfzp1  14480  hash2pwpr  14525  hashge2el2difr  14530  swrdnd2  14703  pfxnd0  14736  repswswrd  14832  relexpsucl  15080  relexpsucr  15081  relexpcnv  15084  relexprelg  15087  relexpdmg  15091  relexprng  15095  relexpfld  15098  relexpaddg  15102  sumz  15770  arisum  15908  arisum2  15909  pwdif  15916  ntrivcvg  15945  prod1  15992  fprodfac  16021  mod2eq1n2dvds  16395  mulsucdiv2z  16401  nn0o1gt2  16429  nno  16430  nn0o  16431  sumeven  16435  sumodd  16436  divalglem1  16442  divalglem6  16446  gcdaddmlem  16570  dfgcd2  16593  mulgcd  16595  lcmf  16680  lcmfunsnlem2lem2  16686  lcmfunsnlem2  16687  prm2orodd  16738  dfphi2  16821  nnnn0modprm0  16853  prm23lt5  16861  oddprmdvds  16950  4sqlem19  17010  ramz  17072  prmolefac  17093  prmgaplem7  17104  cshwshashlem1  17143  ressval3d  17305  ressval3dOLD  17306  firest  17492  xpsfeq  17623  funcres2c  17968  smndex1basss  18940  smndex1mgm  18942  smndex1mndlem  18944  mulgnn0gsum  19120  symgfix2  19458  pmtrprfval  19529  m1expaddsub  19540  psgnprfval  19563  gsumpr  19997  gsumzunsnd  19998  0ringnnzr  20551  sralemOLD  21199  frgpcyg  21615  cnmsgnsubg  21618  psgninv  21623  zrhpsgnelbas  21635  m2detleiblem1  22651  symgmatr01lem  22680  indiscld  23120  pnfnei  23249  mnfnei  23250  alexsubALTlem2  24077  alexsubALTlem3  24078  dscmet  24606  xrtgioo  24847  ishl2  25423  iunmbl2  25611  icombl  25618  ioombl  25619  recnprss  25959  recnperf  25960  dvexp2  26012  dvexp3  26036  dvne0f1  26071  plypf1  26271  taylfvallem1  26416  taylfval  26418  tayl0  26421  coseq0negpitopi  26563  logfac  26661  cxpexp  26728  pythag  26878  reasinsin  26957  harmonicbnd3  27069  lgslem4  27362  gausslemma2dlem0i  27426  lgsquadlem2  27443  2lgslem3  27466  2lgs  27469  2lgsoddprmlem3  27476  2sqnn0  27500  2sqnn  27501  sltres  27725  nolesgn2o  27734  nogesgn1o  27736  nosep1o  27744  nosep2o  27745  noetalem2  27805  ssltun1  27871  ssltun2  27872  eln0s  28376  n0zs  28393  cchhllemOLD  28920  lfgrnloop  29160  uhgr2edg  29243  usgredg4  29252  usgredg2v  29262  usgrexmplef  29294  nb3grprlem1  29415  uvtx01vtx  29432  wlk1walk  29675  upgriswlk  29677  pthdadjvtx  29766  upgrwlkdvdelem  29772  pthdlem2lem  29803  2pthon3v  29976  clwwlkn  30058  clwwlkneq0  30061  eupth2lem3lem4  30263  konigsberg  30289  3vfriswmgrlem  30309  1to2vfriswmgr  30311  1to3vfriswmgr  30312  frgrregorufr0  30356  numclwlk1  30403  ex-pr  30462  shunssi  31400  cvmdi  32356  1neg1t1neg1  32751  iundisj2cnt  32804  fz1nnct  32808  xrge0iifiso  33881  esumpr2  34031  measiuns  34181  sxbrsigalem0  34236  bnj964  34919  subfacval3  35157  kur14lem7  35180  satfrnmapom  35338  gonar  35363  goalr  35365  mrsubcv  35478  nepss  35680  nnuni  35689  fz0n  35693  bccolsum  35701  dfon2lem7  35753  altopthsn  35925  elhf2  36139  nn0prpw  36289  dissym1  36387  ordcmp  36413  bj-currypeirce  36523  bj-jaoi1  36537  bj-jaoi2  36538  bj-ififc  36548  bj-andnotim  36554  bj-nfimexal  36592  bj-sbsb  36803  bj-elsn12g  37026  bj-ideqg1  37130  finxpreclem2  37356  wl-equsal1i  37498  tan2h  37572  poimirlem23  37603  poimirlem32  37612  itg2addnclem  37631  orfa1  38045  orfa2  38046  imaexALTV  38286  inex3  38294  inxpex  38295  mopickr  38319  disjlem14  38754  elpadd0  39766  aks6d1c2p2  42076  sbor2  42205  sn-0ne2  42382  sn-0lt1  42439  hbtlem5  43085  omabs2  43294  safesnsupfiss  43377  safesnsupfidom1o  43379  safesnsupfilb  43380  rp-fakeimass  43474  rp-isfinite6  43480  pr2cv  43510  iunrelexp0  43664  relexpss1d  43667  relexpmulg  43672  iunrelexpmin2  43674  relexp01min  43675  relexp0a  43678  relexpxpmin  43679  relexpaddss  43680  clsk1indlem3  44005  ssrecnpr  44277  seff  44278  sblpnf  44279  expgrowthi  44302  dvconstbi  44303  19.33-2  44351  ax6e2ndeq  44530  en3lpVD  44816  undif3VD  44853  ax6e2ndeqVD  44880  ax6e2ndeqALT  44902  iooinlbub  45419  elprneb  46944  euoreqb  47024  2reu3  47025  afvpcfv0  47061  afvfv0bi  47067  afvco2  47091  afv2orxorb  47143  afv2ndeffv0  47175  afv2fv0b  47181  fvmptrabdm  47208  iccpartltu  47299  iccpartgtl  47300  iccpartgt  47301  iccpartleu  47302  iccpartgel  47303  iccpartnel  47312  elsprel  47349  prsprel  47361  sprsymrelfolem2  47367  paireqne  47385  odz2prm2pw  47437  fmtnofac1  47444  fmtno4prmfac  47446  31prm  47471  lighneallem2  47480  lighneallem3  47481  lighneallem4b  47483  lighneallem4  47484  zeo2ALTV  47545  nn0o1gt2ALTV  47568  nn0oALTV  47570  stgoldbwt  47650  sbgoldbwt  47651  sbgoldbalt  47655  sbgoldbm  47658  sbgoldbo  47661  nnsum3primesle9  47668  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  bgoldbtbndlem1  47679  bgoldbtbnd  47683  tgoldbach  47691  vopnbgrelself  47727  clnbgrgrim  47786  grtriproplem  47790  grtrif1o  47793  grtriclwlk3  47796  upgrwlkupwlk  47863  ztprmneprm  48072  islinindfis  48178  lindslinindsimp2lem5  48191  lindslinindsimp2  48192  lindsrng01  48197  elfzolborelfzop1  48248  flnn0div2ge  48267  blennn0elnn  48311  blen1b  48322  nnolog2flm1  48324  blengt1fldiv2p1  48327  0dig2pr01  48344  dignn0flhalf  48352  nn0sumshdiglemB  48354  nn0sumshdiglem1  48355  resum2sqorgt0  48443  rrx2xpref1o  48452  rrx2plord2  48456  itsclc0yqsol  48498  mosssn  48546  mo0sn  48547  mofsssn  48559  mofmo  48560  f1omo  48574