Theorem syl2anr 609

Description: A double syllogism inference. For an implication-only version, see syl2imc 42. (Contributed by NM, 17-Sep-2013.)

Hypotheses

Ref	Expression
syl2an.1	⊢ (𝜑 → 𝜓)
syl2an.2	⊢ (𝜏 → 𝜒)
syl2an.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syl2anr	⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Proof of Theorem syl2anr

Step	Hyp	Ref	Expression
1		syl2an.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl2an.2	. . 3 ⊢ (𝜏 → 𝜒)
3		syl2an.3	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	1, 2, 3	syl2an 608	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
5	4	ancoms 464	1 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  swopo  5574  ordintdif  6432  funco  6600  resdif  6868  fvcofneq  7117  fnprb  7237  fntpb  7238  fvf1pr  7338  isotr  7367  weisoeq  7388  brrpssg  7765  findsg  7933  coexg  7965  resf1extb  7970  xpexgALT  8017  mpof1o2d  8164  fnsuppres  8236  oaass  8597  oeword  8627  oeworde  8630  mapsnd  8942  ixpssmapg  8984  enrefnn  9102  pw2f1olem  9128  domsdomtr  9159  xpen  9187  mapen  9188  mapdom1  9189  phplem2  9248  mapfienlem1  9424  elfir  9434  wdomen2  9598  carden2b  10075  harcard  10086  isinffi  10100  acnlem  10154  acndom  10157  alephdom  10187  fin23lem21  10444  fin23lem39  10455  isf32lem5  10462  fin1a2lem12  10516  axdc3lem2  10556  ttukeylem1  10614  pwcfsdom  10695  canthp1  10766  nqereu  11041  addpqf  11056  axmulf  11258  axmulass  11269  axdistr  11270  ltaddnegr  11554  negeu  11574  fimaxre3  12290  nnsub  12409  nn0sub  12683  ltsubnn0  12684  elz2  12738  uzaddcl  13058  qaddcl  13120  xltneg  13374  xleneg  13375  supxrbnd1  13478  infxrgelb  13493  iccneg  13630  uzsubsubfz  13707  fzsplit2  13710  fzadd2  13720  fzss1  13724  uzsplit  13757  fzdif1  13766  fz0fzdiffz0  13798  difelfzle  13802  difelfznle  13803  fvffz0  13807  preduz  13811  predfz  13814  fzonlt0  13844  fzouzsplit  13856  fzo0addelr  13881  eluzgtdifelfzo  13889  elfzodifsumelfzo  13893  ssfzo12  13921  elfznelfzob  13936  fllt  13973  flflp1  13974  uzsup  14030  negmod  14086  modifeq2int  14103  modfzo0difsn  14113  modsumfzodifsn  14114  om2uzlt2i  14121  nn0ennn  14149  suppssfz  14164  seqfveq2  14194  sermono  14204  seqf1o  14213  ser1const  14228  rpexpmord  14338  mulsubdivbinom2  14433  faclbnd  14461  bcval4  14478  bcpasc  14492  hashkf  14503  hashunx  14557  fz1isolem  14633  ishashinf  14635  seqcoll  14636  ccatval1  14749  ccatval21sw  14758  ccatrn  14762  ccatalpha  14767  swrdnd0  14835  swrd0  14836  swrdfv2  14839  swrdspsleq  14843  addlenpfx  14868  ccatpfx  14878  swrdswrd  14882  pfxccatin12lem2  14908  pfxccat3  14911  swrdccat  14912  revccat  14943  repswswrd  14963  cshwmodn  14974  cshwidxmod  14982  repswcshw  14991  2cshwid  14993  2cshwcom  14995  2cshwcshw  15004  cshwcshid  15006  cshwcsh2id  15007  s1co  15012  cshco  15015  trclub  15180  shftfval  15252  seqshft  15267  crim  15311  caubnd  15555  limsuplt  15675  isercolllem2  15862  fsumcvg  15907  fsumcvg2  15922  fsumshftm  15976  fsumo1  16008  isumshft  16037  harmonic  16057  cvgrat  16081  mertenslem1  16082  zprod  16133  fprodmodd  16193  bpolylem  16243  bpolysum  16248  bpolydiflem  16249  fsumkthpow  16251  rpnnen2lem12  16422  dvdsval3  16455  negdvdsb  16471  dvdsnegb  16472  dvdsmul1  16476  dvdsabseq  16512  dvdsssfz1  16517  odd2np1  16540  divalglem8  16599  ndvdsadd  16609  dfgcd2  16748  dvdssqim  16756  nn0seqcvgd  16774  seq1st  16775  algcvgblem  16781  lcmf  16837  lcmfunsnlem2  16844  cncongr2  16872  prmdvdsfz  16910  isprm7  16913  prmndvdsfaclt  16930  powm2modprm  17010  modprm0  17012  modprmn0modprm0  17014  pythagtriplem1  17023  pythagtriplem4  17026  pythagtriplem8  17030  pythagtriplem9  17031  pythagtriplem12  17033  pythagtriplem14  17035  pythagtriplem16  17037  pcexp  17066  pc2dvds  17086  pcz  17088  fldivp1  17104  pcfac  17106  oddprmdvds  17110  pockthg  17113  infpnlem1  17117  prmreclem1  17123  prmreclem2  17124  1arith  17134  4sqlem11  17162  vdwlem2  17189  vdwlem8  17195  vdwnnlem2  17203  prmgaplem7  17264  prmgaplem8  17265  cshwshashlem2  17303  cshwshashlem3  17304  pwsval  17686  isacs1i  17860  funcsetcestrclem9  18366  ismgmid  18874  mgmhmpropd  18916  mhmpropd  19016  smndex1gid  19129  smndex1gidOLD  19130  smndex1id  19139  grpsubid1  19264  mulgnnp1  19321  mulgsubcl  19327  mulgnn0z  19340  mulgnndir  19342  mulgneg2  19347  lagsubg  19439  ghmco  19479  symg2bas  19637  symgextfv  19662  pgpfi2  19850  efgsfo  19983  frgpupf  20017  frgpup1  20019  gsummptshft  20180  telgsumfzslem  20232  telgsums  20237  ablfac1eu  20319  pgpfac1lem2  20321  ablfaclem3  20333  dvdsrid  20627  dvdsrneg  20630  dvr1  20667  abv1  21112  lmodfopne  21205  lbsexg  21472  xrsds  21746  znf1o  21887  lindfmm  22163  lindsdom  22186  lindsenlbs  22187  gsummoncoe1  22656  matecl  22770  mavmul0g  22898  gsummatr01  23004  matunitlindflem2  23025  mp2pm2mplem4  23157  chfacfisf  23202  chfacfisfcpmat  23203  chfacfpmmulgsum2  23213  cpmadugsumlemF  23224  isclo  23435  resttopon  23509  restcld  23520  restcls  23529  iscn  23583  iscnp  23585  cnco  23614  cndis  23639  cnindis  23640  cmpsub  23748  hauscmplem  23754  cmpfii  23757  ptcnplem  23970  txtube  23989  txcmplem1  23990  xkoptsub  24003  qtoptop  24049  kqfval  24072  hmeoco  24121  fileln0  24199  trfil1  24235  trfil2  24236  trufil  24259  elfm3  24299  hausflf2  24347  isucn  24626  bl2in  24749  metss2lem  24860  metss2  24861  stdbdxmet  24864  metrest  24873  nmval2  24941  nmoix  25078  ioo2bl  25142  xrsxmet  25159  expcn  25223  elcncf  25240  icccvx  25301  cphsscph  25602  iscmet3  25644  causs  25649  metcld2  25658  metsscmetcld  25666  cncmet  25673  bcth3  25682  ovolgelb  25831  ovolfi  25845  shft2rab  25859  uniioombllem3  25936  dyadmax  25949  dyadmbl  25951  subopnmbl  25955  volcn  25957  mbfid  25986  mbfeqalem2  25993  mbfres  25995  cnmbf  26010  i1fmulc  26054  mbfi1fseqlem3  26068  mbfi1fseqlem4  26069  itg2seq  26093  itg2gt0  26111  itgss3  26165  dvexp  26303  plypow  26553  plyeq0lem  26559  coeidlem  26586  dgrlt  26615  dgrcolem2  26623  elqaalem2  26673  aacjcl  26684  aaliou3lem1  26699  aaliou3lem2  26700  pserdvlem2  26785  abelthlem8  26796  cosord  26889  sinord  26892  resinf1o  26894  relogexp  26954  logdivlt  26979  advlogexp  27013  logcxp  27027  cxpcl  27032  rpcxpcl  27034  cxpne0  27035  logbchbase  27129  logbgt0b  27151  birthdaylem2  27310  cxplim  27329  divsqrtsumo1  27341  zetacvg  27372  wilthlem1  27425  ftalem7  27436  basellem1  27438  issqf  27493  sqf11  27496  sgmf  27502  sgmnncl  27504  sqff1o  27539  dvdsflsumcom  27545  mpodvdsmulf1o  27551  dvdsmulf1o  27553  sgmppw  27554  chtublem  27568  chtub  27569  logexprlim  27582  bposlem3  27643  bposlem5  27645  bposlem6  27646  lgsdirnn0  27701  gausslemma2dlem1a  27722  gausslemma2dlem5a  27727  lgsquad2  27743  lgsquad3  27744  2sqreulem1  27803  2sqreunnlem1  27806  dchrisumlem1  27846  dchrisumlem2  27847  dchrisumlem3  27848  mulogsumlem  27888  fltoprm  28025  noextenddif  28055  addsrid  28380  ltnegs  28461  lenegs  28462  om2noseqlt2  28716  elzn0s  28814  eln0zs  28816  peano5uzs  28820  bdayfinbndlem1  28883  brbtwn  29507  uspgrupgrushgr  29790  usgrumgruspgr  29793  cusgrfilem2  30067  finsumvtxdg2ssteplem2  30157  pthhashvtx  30345  cyclnumvtx  30418  crctcshwlkn0lem4  30432  crctcshwlkn0lem6  30434  crctcshwlkn0lem7  30435  crctcshwlkn0  30440  elwspths2spth  30589  rusgrnumwwlk  30597  clwlkclwwlklem2fv2  30617  erclwwlknref  30690  1to2vfriswmgr  30910  4cycl2v2nb  30920  frgr2wwlkeqm  30962  nvo00  31393  nmorepnf  31400  ubthlem1  31502  normpyc  31778  occon3  31929  pjpreeq  32030  idcnop  32613  riesz3i  32694  cnlnssadj  32712  rnbra  32739  strlem3a  32884  cvcon3  32916  ssdmd1  32945  ssdmd2  32946  relfi  33268  fcobijfs2  33384  fzsplit3  33455  prmsimpcyc  33859  esumcst  34765  dmvlsiga  34831  ballotlemimin  35208  bnj545  35595  bnj929  35636  bnj953  35639  fineqvnttrclselem1  35889  derangsn  36102  iscvm  36191  cvmsval  36198  cvmliftlem7  36223  cvmlift2lem12  36246  mclsssvlem  36494  supfz  36672  faclimlem3  36688  opnrebl2  37287  nn0prpwlem  37288  tailval  37339  nndivlub  37424  ctbssinf  38521  finixpnum  38720  ltflcei  38723  poimirlem4  38734  poimirlem14  38744  poimirlem15  38745  poimirlem19  38749  poimirlem20  38750  poimirlem22  38752  poimirlem24  38754  poimirlem28  38758  poimirlem30  38760  poimirlem31  38761  mblfinlem2  38768  mblfinlem3  38769  mblfinlem4  38770  ftc1anclem1  38803  ftc1anclem4  38806  ftc1anclem5  38807  ftc1anclem7  38809  ftc1anclem8  38810  ftc1anc  38811  caushft  38887  ismtyval  38926  heiborlem7  38943  heiborlem10  38946  heibor  38947  lcmineqlem8  43278  deg1gprod  43382  oexpreposd  43572  elrfirn  43899  ismrc  43905  nacsfix  43916  mzpcompact2lem  43955  eldiophb  43961  ellz1  43971  rexrabdioph  43994  congrep  44173  jm2.26a  44200  rngunsnply  44363  mendring  44382  iocmbl  44407  oeord2lim  44503  cantnfresb  44518  omabs2  44526  ofoafg  44548  dfno2  44621  rp-isfinite5  44710  enrelmap  45189  expgrowthi  45509  hashnnltb  46208  cnfex  46250  xlimclim2lem  47054  climxlim2  47061  icccncfext  47102  itgsinexp  47170  iblspltprt  47188  itgspltprt  47194  fourierdlem50  47371  fourierswlem  47445  etransclem35  47484  zm1nn  48577  subsubelfzo0  48602  ceilbi  48612  addmodne  48625  m1modmmod  48639  modlt0b  48644  iccpartres  48705  iccelpart  48720  iccpartiun  48721  iccpartnel  48725  nprmmul1  48814  goldbachthlem1  48835  goldbachth  48837  odz2prm2pw  48853  2pwp1prm  48879  evenltle  49020  fpprwpprb  49043  sbgoldbaltlem2  49083  bgoldbachlt  49116  isubgredg  49169  gricushgr  49220  uhgrimisgrgriclem  49233  gpgvtx0  49356  gpg5nbgrvtx13starlem2  49375  upgrwlkupwlk  49443  2zrngamgm  49547  lincresunit3  49798  lincreslvec3  49799  isldepslvec2  49802  blengt1fldiv2p1  49910  dignn0flhalf  49935  nn0sumshdiglemA  49936  rrx2pnedifcoorneor  50034  precofval2  50709  aacllem  51219