Theorem jaoi 853

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

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 844

This theorem is referenced by:  jao1i  854  jaod  855  pm1.4  865  pm3.2ni  877  pm1.2  900  pm2.4  903  pm2.41  904  orim12i  905  pm1.5  916  pm2.42  939  jaoa  952  jaoian  953  pm4.44  993  andi  1004  ecase3  1028  cases2ALT  1045  consensus  1049  jaoi3  1057  1fpid3  1080  19.33  1888  19.33b  1889  nfim1  2195  dfsb2  2497  mooran1  2555  eueq3  3641  sbcor  3764  sspss  4030  sspsstr  4036  elun  4079  ssun  4119  inss  4169  raaan2  4452  ifbi  4478  ifcomnan  4512  elpr2OLD  4584  rabsnifsb  4655  tpprceq3  4734  tppreqb  4735  pwpw0  4743  sssn  4756  snsssn  4769  preq12b  4778  prnebg  4783  preq12nebg  4790  elpr2elpr  4796  pwsnOLD  4829  prproe  4834  3elpr2eq  4835  unissint  4900  zfpair  5339  propeqop  5415  propssopi  5416  opthhausdorff  5425  opthhausdorff0  5426  iunopeqop  5429  relsnb  5701  iresn0n0  5952  sotri2  6023  sotri3  6024  somincom  6028  ordssun  6350  unizlim  6368  onxpdisj  6371  tpres  7058  sorpssuni  7563  ordeleqon  7609  ordunisuc  7654  orduninsuc  7665  tfinds  7681  limomss  7692  limom  7703  soxp  7941  ressuppssdif  7972  tfr2b  8198  omopthi  8451  domnsym  8839  brwdom  9256  cantnfvalf  9353  trpredlem1  9405  trpred0  9410  djuss  9609  djuunxp  9610  eldju2ndl  9613  eldju2ndr  9614  djuun  9615  updjud  9623  iscard3  9780  cflim2  9950  sornom  9964  isfin5  9986  isfin6  9987  sdom2en01  9989  fin23lem29  10028  fin23lem30  10029  fin56  10080  fin67  10082  hsmexlem9  10112  axcc4dom  10128  axdc3lem2  10138  axdc3lem4  10140  brdom3  10215  winainflem  10380  r1tskina  10469  indpi  10594  ltxrlt  10976  nn0sub  12213  nn0n0n1ge2b  12231  nn0ge2m1nn  12232  xnn0xr  12240  xnn0nemnf  12246  elnn0z  12262  nn0lt10b  12312  nn0le2is012  12314  nn0ind-raph  12350  uzin  12547  indstr2  12596  nn0ledivnn  12772  xrnemnf  12782  xrnepnf  12783  mnfltxr  12792  xnn0n0n1ge2b  12796  xnn0ge0  12798  xnn0xaddcl  12898  xnn0lenn0nn0  12908  xnn0xadd0  12910  xmullem2  12928  rexmul  12934  xnn0xrge0  13167  elfzonlteqm1  13391  elfznelfzo  13420  injresinjlem  13435  injresinj  13436  fldiv4p1lem1div2  13483  fldiv4lem1div2  13485  modfzo0difsn  13591  ssnn0fi  13633  fsuppmapnn0fiubex  13640  m1expcl2  13732  m1expeven  13758  sq01  13868  expnngt1  13884  nn0opthi  13912  facp1  13920  faclbnd3  13934  faclbnd4lem1  13935  faclbnd4lem3  13937  bcn1  13955  hashnemnf  13986  hashv01gt1  13987  hashneq0  14007  hashrabrsn  14015  hashrabsn01  14016  hashrabsn1  14017  hashunx  14029  hashsnle1  14060  hashfzp1  14074  hash2pwpr  14118  hashge2el2difr  14123  swrdnd2  14296  pfxnd0  14329  repswswrd  14425  relexpsucl  14670  relexpsucr  14671  relexpcnv  14674  relexprelg  14677  relexpdmg  14681  relexprng  14685  relexpfld  14688  relexpaddg  14692  sumz  15362  arisum  15500  arisum2  15501  pwdif  15508  ntrivcvg  15537  prod1  15582  fprodfac  15611  mod2eq1n2dvds  15984  mulsucdiv2z  15990  nn0o1gt2  16018  nno  16019  nn0o  16020  sumeven  16024  sumodd  16025  divalglem1  16031  divalglem6  16035  gcdaddmlem  16159  dfgcd2  16182  mulgcd  16184  lcmf  16266  lcmfunsnlem2lem2  16272  lcmfunsnlem2  16273  prm2orodd  16324  dfphi2  16403  nnnn0modprm0  16435  prm23lt5  16443  oddprmdvds  16532  4sqlem19  16592  ramz  16654  prmolefac  16675  prmgaplem7  16686  cshwshashlem1  16725  ressval3d  16882  ressval3dOLD  16883  firest  17060  xpsfeq  17191  funcres2c  17533  smndex1basss  18459  smndex1mgm  18461  smndex1mndlem  18463  mulgnn0gsum  18625  symgfix2  18939  pmtrprfval  19010  m1expaddsub  19021  psgnprfval  19044  gsumpr  19471  gsumzunsnd  19472  sralemOLD  20355  0ringnnzr  20453  frgpcyg  20693  cnmsgnsubg  20694  psgninv  20699  zrhpsgnelbas  20711  m2detleiblem1  21681  symgmatr01lem  21710  indiscld  22150  pnfnei  22279  mnfnei  22280  alexsubALTlem2  23107  alexsubALTlem3  23108  dscmet  23634  xrtgioo  23875  ishl2  24439  iunmbl2  24626  icombl  24633  ioombl  24634  recnprss  24973  recnperf  24974  dvexp2  25023  dvexp3  25047  dvne0f1  25081  plypf1  25278  taylfvallem1  25421  taylfval  25423  tayl0  25426  coseq0negpitopi  25565  logfac  25661  cxpexp  25728  pythag  25872  reasinsin  25951  harmonicbnd3  26062  lgslem4  26353  gausslemma2dlem0i  26417  lgsquadlem2  26434  2lgslem3  26457  2lgs  26460  2lgsoddprmlem3  26467  2sqnn0  26491  2sqnn  26492  cchhllemOLD  27158  lfgrnloop  27398  uhgr2edg  27478  usgredg4  27487  usgredg2v  27497  usgrexmplef  27529  nb3grprlem1  27650  uvtx01vtx  27667  wlk1walk  27908  upgriswlk  27910  pthdadjvtx  27999  upgrwlkdvdelem  28005  pthdlem2lem  28036  2pthon3v  28209  clwwlkn  28291  clwwlkneq0  28294  eupth2lem3lem4  28496  konigsberg  28522  3vfriswmgrlem  28542  1to2vfriswmgr  28544  1to3vfriswmgr  28545  frgrregorufr0  28589  numclwlk1  28636  ex-pr  28695  shunssi  29631  cvmdi  30587  1neg1t1neg1  30974  iundisj2cnt  31022  fz1nnct  31026  xrge0iifiso  31787  esumpr2  31935  measiuns  32085  sxbrsigalem0  32138  bnj964  32823  subfacval3  33051  kur14lem7  33074  satfrnmapom  33232  gonar  33257  goalr  33259  mrsubcv  33372  nepss  33564  nnuni  33595  fz0n  33602  bccolsum  33611  dfon2lem7  33671  ttrclselem1  33711  sltres  33792  nolesgn2o  33801  nogesgn1o  33803  nosep1o  33811  nosep2o  33812  noetalem2  33872  ssltun1  33929  ssltun2  33930  altopthsn  34190  elhf2  34404  nn0prpw  34439  dissym1  34537  ordcmp  34563  bj-currypeirce  34664  bj-jaoi1  34679  bj-jaoi2  34680  bj-ififc  34690  bj-andnotim  34697  bj-nfimexal  34734  bj-sbsb  34947  bj-elsn12g  35158  bj-ideqg1  35262  finxpreclem2  35488  wl-equsal1i  35629  tan2h  35696  poimirlem23  35727  poimirlem32  35736  itg2addnclem  35755  orfa1  36170  orfa2  36171  imaexALTV  36392  inex3  36400  inxpex  36401  elpadd0  37750  sbor2  40105  sn-0ne2  40310  sn-0lt1  40353  hbtlem5  40869  rp-fakeimass  41017  rp-isfinite6  41023  pr2cv  41044  iunrelexp0  41199  relexpss1d  41202  relexpmulg  41207  iunrelexpmin2  41209  relexp01min  41210  relexp0a  41213  relexpxpmin  41214  relexpaddss  41215  clsk1indlem3  41542  ssrecnpr  41815  seff  41816  sblpnf  41817  expgrowthi  41840  dvconstbi  41841  19.33-2  41889  ax6e2ndeq  42068  en3lpVD  42354  undif3VD  42391  ax6e2ndeqVD  42418  ax6e2ndeqALT  42440  iooinlbub  42929  elprneb  44410  euoreqb  44488  2reu3  44489  afvpcfv0  44525  afvfv0bi  44531  afvco2  44555  afv2orxorb  44607  afv2ndeffv0  44639  afv2fv0b  44645  fvmptrabdm  44672  iccpartltu  44765  iccpartgtl  44766  iccpartgt  44767  iccpartleu  44768  iccpartgel  44769  iccpartnel  44778  elsprel  44815  prsprel  44827  sprsymrelfolem2  44833  paireqne  44851  odz2prm2pw  44903  fmtnofac1  44910  fmtno4prmfac  44912  31prm  44937  lighneallem2  44946  lighneallem3  44947  lighneallem4b  44949  lighneallem4  44950  zeo2ALTV  45011  nn0o1gt2ALTV  45034  nn0oALTV  45036  stgoldbwt  45116  sbgoldbwt  45117  sbgoldbalt  45121  sbgoldbm  45124  sbgoldbo  45127  nnsum3primesle9  45134  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  bgoldbtbndlem1  45145  bgoldbtbnd  45149  tgoldbach  45157  isomuspgrlem1  45167  upgrwlkupwlk  45190  ztprmneprm  45571  islinindfis  45678  lindslinindsimp2lem5  45691  lindslinindsimp2  45692  lindsrng01  45697  elfzolborelfzop1  45748  flnn0div2ge  45767  blennn0elnn  45811  blen1b  45822  nnolog2flm1  45824  blengt1fldiv2p1  45827  0dig2pr01  45844  dignn0flhalf  45852  nn0sumshdiglemB  45854  nn0sumshdiglem1  45855  resum2sqorgt0  45943  rrx2xpref1o  45952  rrx2plord2  45956  itsclc0yqsol  45998  mosssn  46048  mo0sn  46049  mofsssn  46061  mofmo  46062  f1omo  46076