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  5570  ordintdif  6414  funco  6580  resdif  6846  fvcofneq  7093  fnprb  7214  fntpb  7215  fvf1pr  7315  isotr  7344  weisoeq  7365  brrpssg  7741  findsg  7909  coexg  7941  resf1extb  7946  xpexgALT  7993  mpof1o2d  8137  fnsuppres  8208  oaass  8569  oeword  8599  oeworde  8602  mapsnd  8914  ixpssmapg  8956  enrefnn  9074  pw2f1olem  9100  domsdomtr  9131  xpen  9159  mapen  9160  mapdom1  9161  phplem2  9220  mapfienlem1  9397  elfir  9407  wdomen2  9571  carden2b  10048  harcard  10059  isinffi  10073  acnlem  10127  acndom  10130  alephdom  10160  fin23lem21  10417  fin23lem39  10428  isf32lem5  10435  fin1a2lem12  10489  axdc3lem2  10529  ttukeylem1  10587  pwcfsdom  10668  canthp1  10739  nqereu  11014  addpqf  11029  axmulf  11231  axmulass  11242  axdistr  11243  ltaddnegr  11527  negeu  11547  fimaxre3  12263  nnsub  12382  nn0sub  12656  ltsubnn0  12657  elz2  12711  uzaddcl  13031  qaddcl  13093  xltneg  13347  xleneg  13348  supxrbnd1  13451  infxrgelb  13466  iccneg  13603  uzsubsubfz  13680  fzsplit2  13683  fzadd2  13693  fzss1  13697  uzsplit  13730  fzdif1  13739  fz0fzdiffz0  13771  difelfzle  13775  difelfznle  13776  fvffz0  13780  preduz  13784  predfz  13787  fzonlt0  13817  fzouzsplit  13829  fzo0addelr  13854  eluzgtdifelfzo  13862  elfzodifsumelfzo  13866  ssfzo12  13894  elfznelfzob  13909  fllt  13946  flflp1  13947  uzsup  14003  negmod  14059  modifeq2int  14076  modfzo0difsn  14086  modsumfzodifsn  14087  om2uzlt2i  14094  nn0ennn  14122  suppssfz  14137  seqfveq2  14167  sermono  14177  seqf1o  14186  ser1const  14201  rpexpmord  14311  mulsubdivbinom2  14406  faclbnd  14434  bcval4  14451  bcpasc  14465  hashkf  14476  hashunx  14530  fz1isolem  14606  ishashinf  14608  seqcoll  14609  ccatval1  14722  ccatval21sw  14731  ccatrn  14735  ccatalpha  14740  swrdnd0  14807  swrd0  14808  swrdfv2  14811  swrdspsleq  14815  addlenpfx  14840  ccatpfx  14850  swrdswrd  14854  pfxccatin12lem2  14880  pfxccat3  14883  swrdccat  14884  revccat  14915  repswswrd  14935  cshwmodn  14946  cshwidxmod  14954  repswcshw  14963  2cshwid  14965  2cshwcom  14967  2cshwcshw  14976  cshwcshid  14978  cshwcsh2id  14979  s1co  14984  cshco  14987  trclub  15151  shftfval  15223  seqshft  15238  crim  15282  caubnd  15526  limsuplt  15646  isercolllem2  15833  fsumcvg  15878  fsumcvg2  15893  fsumshftm  15947  fsumo1  15979  isumshft  16008  harmonic  16028  cvgrat  16052  mertenslem1  16053  zprod  16104  fprodmodd  16164  bpolylem  16214  bpolysum  16219  bpolydiflem  16220  fsumkthpow  16222  rpnnen2lem12  16393  dvdsval3  16426  negdvdsb  16442  dvdsnegb  16443  dvdsmul1  16447  dvdsabseq  16483  dvdsssfz1  16488  odd2np1  16511  divalglem8  16570  ndvdsadd  16580  dfgcd2  16719  dvdssqim  16727  nn0seqcvgd  16745  seq1st  16746  algcvgblem  16752  lcmf  16808  lcmfunsnlem2  16815  cncongr2  16843  prmdvdsfz  16881  isprm7  16884  prmndvdsfaclt  16901  powm2modprm  16981  modprm0  16983  modprmn0modprm0  16985  pythagtriplem1  16994  pythagtriplem4  16997  pythagtriplem8  17001  pythagtriplem9  17002  pythagtriplem12  17004  pythagtriplem14  17006  pythagtriplem16  17008  pcexp  17037  pc2dvds  17057  pcz  17059  fldivp1  17075  pcfac  17077  oddprmdvds  17081  pockthg  17084  infpnlem1  17088  prmreclem1  17094  prmreclem2  17095  1arith  17105  4sqlem11  17133  vdwlem2  17160  vdwlem8  17166  vdwnnlem2  17174  prmgaplem7  17235  prmgaplem8  17236  cshwshashlem2  17274  cshwshashlem3  17275  pwsval  17657  isacs1i  17831  funcsetcestrclem9  18337  ismgmid  18845  mgmhmpropd  18887  mhmpropd  18987  smndex1gid  19100  smndex1gidOLD  19101  smndex1id  19110  grpsubid1  19235  mulgnnp1  19292  mulgsubcl  19298  mulgnn0z  19311  mulgnndir  19313  mulgneg2  19318  lagsubg  19410  ghmco  19450  symg2bas  19607  symgextfv  19632  pgpfi2  19820  efgsfo  19953  frgpupf  19987  frgpup1  19989  gsummptshft  20150  telgsumfzslem  20202  telgsums  20207  ablfac1eu  20289  pgpfac1lem2  20291  ablfaclem3  20303  dvdsrid  20597  dvdsrneg  20600  dvr1  20637  abv1  21082  lmodfopne  21175  lbsexg  21442  xrsds  21716  znf1o  21857  lindfmm  22133  lindsdom  22156  lindsenlbs  22157  gsummoncoe1  22626  matecl  22740  mavmul0g  22868  gsummatr01  22974  matunitlindflem2  22995  mp2pm2mplem4  23127  chfacfisf  23172  chfacfisfcpmat  23173  chfacfpmmulgsum2  23183  cpmadugsumlemF  23194  isclo  23405  resttopon  23479  restcld  23490  restcls  23499  iscn  23553  iscnp  23555  cnco  23584  cndis  23609  cnindis  23610  cmpsub  23718  hauscmplem  23724  cmpfii  23727  ptcnplem  23940  txtube  23959  txcmplem1  23960  xkoptsub  23973  qtoptop  24019  kqfval  24042  hmeoco  24091  fileln0  24169  trfil1  24205  trfil2  24206  trufil  24229  elfm3  24269  hausflf2  24317  isucn  24596  bl2in  24719  metss2lem  24830  metss2  24831  stdbdxmet  24834  metrest  24843  nmval2  24911  nmoix  25048  ioo2bl  25112  xrsxmet  25129  expcn  25193  elcncf  25210  icccvx  25271  cphsscph  25572  iscmet3  25614  causs  25619  metcld2  25628  metsscmetcld  25636  cncmet  25643  bcth3  25652  ovolgelb  25801  ovolfi  25815  shft2rab  25829  uniioombllem3  25906  dyadmax  25919  dyadmbl  25921  subopnmbl  25925  volcn  25927  mbfid  25956  mbfeqalem2  25963  mbfres  25965  cnmbf  25980  i1fmulc  26024  mbfi1fseqlem3  26038  mbfi1fseqlem4  26039  itg2seq  26063  itg2gt0  26081  itgss3  26135  dvexp  26273  plypow  26523  plyeq0lem  26529  coeidlem  26556  dgrlt  26585  dgrcolem2  26593  elqaalem2  26643  aacjcl  26654  aaliou3lem1  26669  aaliou3lem2  26670  pserdvlem2  26755  abelthlem8  26766  cosord  26859  sinord  26862  resinf1o  26864  relogexp  26924  logdivlt  26949  advlogexp  26983  logcxp  26997  cxpcl  27002  rpcxpcl  27004  cxpne0  27005  logbchbase  27099  logbgt0b  27121  birthdaylem2  27280  cxplim  27299  divsqrtsumo1  27311  zetacvg  27342  wilthlem1  27395  ftalem7  27406  basellem1  27408  issqf  27463  sqf11  27466  sgmf  27472  sgmnncl  27474  sqff1o  27509  dvdsflsumcom  27515  mpodvdsmulf1o  27521  dvdsmulf1o  27523  sgmppw  27524  chtublem  27538  chtub  27539  logexprlim  27552  bposlem3  27613  bposlem5  27615  bposlem6  27616  lgsdirnn0  27671  gausslemma2dlem1a  27692  gausslemma2dlem5a  27697  lgsquad2  27713  lgsquad3  27714  2sqreulem1  27773  2sqreunnlem1  27776  dchrisumlem1  27816  dchrisumlem2  27817  dchrisumlem3  27818  mulogsumlem  27858  fltoprm  27995  noextenddif  28025  addsrid  28350  ltnegs  28431  lenegs  28432  om2noseqlt2  28686  elzn0s  28784  eln0zs  28786  peano5uzs  28790  bdayfinbndlem1  28853  brbtwn  29477  uspgrupgrushgr  29760  usgrumgruspgr  29763  cusgrfilem2  30037  finsumvtxdg2ssteplem2  30127  pthhashvtx  30315  cyclnumvtx  30388  crctcshwlkn0lem4  30402  crctcshwlkn0lem6  30404  crctcshwlkn0lem7  30405  crctcshwlkn0  30410  elwspths2spth  30559  rusgrnumwwlk  30567  clwlkclwwlklem2fv2  30587  erclwwlknref  30660  1to2vfriswmgr  30880  4cycl2v2nb  30890  frgr2wwlkeqm  30932  nvo00  31363  nmorepnf  31370  ubthlem1  31472  normpyc  31748  occon3  31899  pjpreeq  32000  idcnop  32583  riesz3i  32664  cnlnssadj  32682  rnbra  32709  strlem3a  32854  cvcon3  32886  ssdmd1  32915  ssdmd2  32916  relfi  33196  fcobijfs2  33314  fzsplit3  33385  prmsimpcyc  33789  esumcst  34695  dmvlsiga  34761  ballotlemimin  35138  bnj545  35525  bnj929  35566  bnj953  35569  fineqvnttrclselem1  35789  derangsn  35935  iscvm  36024  cvmsval  36031  cvmliftlem7  36056  cvmlift2lem12  36079  mclsssvlem  36327  supfz  36494  faclimlem3  36510  opnrebl2  37109  nn0prpwlem  37110  tailval  37161  nndivlub  37246  ctbssinf  38329  finixpnum  38528  ltflcei  38531  poimirlem4  38542  poimirlem14  38552  poimirlem15  38553  poimirlem19  38557  poimirlem20  38558  poimirlem22  38560  poimirlem24  38562  poimirlem28  38566  poimirlem30  38568  poimirlem31  38569  mblfinlem2  38576  mblfinlem3  38577  mblfinlem4  38578  ftc1anclem1  38611  ftc1anclem4  38614  ftc1anclem5  38615  ftc1anclem7  38617  ftc1anclem8  38618  ftc1anc  38619  caushft  38695  ismtyval  38734  heiborlem7  38751  heiborlem10  38754  heibor  38755  lcmineqlem8  43086  deg1gprod  43190  oexpreposd  43379  elrfirn  43705  ismrc  43711  nacsfix  43722  mzpcompact2lem  43761  eldiophb  43767  ellz1  43777  rexrabdioph  43800  congrep  43979  jm2.26a  44006  rngunsnply  44170  mendring  44189  iocmbl  44214  oeord2lim  44310  cantnfresb  44325  omabs2  44333  ofoafg  44355  dfno2  44428  rp-isfinite5  44517  enrelmap  44996  expgrowthi  45316  hashnnltb  46012  cnfex  46044  xlimclim2lem  46848  climxlim2  46855  icccncfext  46896  itgsinexp  46964  iblspltprt  46982  itgspltprt  46988  fourierdlem50  47165  fourierswlem  47239  etransclem35  47278  zm1nn  48371  subsubelfzo0  48396  ceilbi  48406  addmodne  48419  m1modmmod  48433  modlt0b  48438  iccpartres  48499  iccelpart  48514  iccpartiun  48515  iccpartnel  48519  nprmmul1  48608  goldbachthlem1  48629  goldbachth  48631  odz2prm2pw  48647  2pwp1prm  48673  evenltle  48814  fpprwpprb  48837  sbgoldbaltlem2  48877  bgoldbachlt  48910  isubgredg  48963  gricushgr  49014  uhgrimisgrgriclem  49027  gpgvtx0  49150  gpg5nbgrvtx13starlem2  49169  upgrwlkupwlk  49237  2zrngamgm  49341  lincresunit3  49592  lincreslvec3  49593  isldepslvec2  49596  blengt1fldiv2p1  49704  dignn0flhalf  49729  nn0sumshdiglemA  49730  rrx2pnedifcoorneor  49827  precofval2  50476  aacllem  50938