Theorem syl2anr 598

Description: A double syllogism inference. For an implication-only version, see syl2imc 41. (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 597	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
5	4	ancoms 461	1 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  swopo  5486  ordintdif  6242  funco  6397  resdif  6637  fvcofneq  6861  fnprb  6973  fntpb  6974  isotr  7091  weisoeq  7110  brrpssg  7453  findsg  7611  coexg  7636  xpexgALT  7684  fnsuppres  7859  wfrlem10  7966  oaass  8189  oeword  8218  oeworde  8221  mapsnd  8452  ixpssmapg  8494  pw2f1olem  8623  domsdomtr  8654  xpen  8682  mapen  8683  mapdom1  8684  mapfienlem1  8870  elfir  8881  wdomen2  9043  carden2b  9398  harcard  9409  isinffi  9423  acnlem  9476  acndom  9479  alephdom  9509  fin23lem21  9763  fin23lem39  9774  isf32lem5  9781  fin1a2lem12  9835  axdc3lem2  9875  ttukeylem1  9933  pwcfsdom  10007  canthp1  10078  nqereu  10353  addpqf  10368  axmulf  10570  axmulass  10581  axdistr  10582  ltaddnegr  10858  negeu  10878  fimaxre3  11589  nnsub  11684  nn0sub  11950  ltsubnn0  11951  elz2  12002  uzaddcl  12307  qaddcl  12367  xltneg  12613  xleneg  12614  supxrbnd1  12717  infxrgelb  12731  iccneg  12861  uzsubsubfz  12932  fzsplit2  12935  fzadd2  12945  fzss1  12949  uzsplit  12982  fz0fzdiffz0  13019  difelfzle  13023  difelfznle  13024  fvffz0  13028  preduz  13032  predfz  13035  fzonlt0  13063  fzouzsplit  13075  fzo0addelr  13095  eluzgtdifelfzo  13102  elfzodifsumelfzo  13106  ssfzo12  13133  elfznelfzob  13146  fllt  13179  flflp1  13180  uzsup  13234  negmod  13287  modifeq2int  13304  modfzo0difsn  13314  modsumfzodifsn  13315  om2uzlt2i  13322  nn0ennn  13350  suppssfz  13365  seqfveq2  13395  sermono  13405  seqf1o  13414  ser1const  13429  rpexpmord  13535  mulsubdivbinom2  13625  faclbnd  13653  bcval4  13670  bcpasc  13684  hashkf  13695  hashunx  13750  hashfacen  13815  fz1isolem  13822  ishashinf  13824  seqcoll  13825  ccatval1  13932  ccatval21sw  13941  ccatrn  13945  ccatalpha  13949  swrdnd0  14021  swrd0  14022  swrdfv2  14025  swrdspsleq  14029  addlenpfx  14055  ccatpfx  14065  swrdswrd  14069  pfxccatin12lem2  14095  pfxccat3  14098  swrdccat  14099  revccat  14130  repswswrd  14148  cshwmodn  14159  cshwidxmod  14167  repswcshw  14176  2cshwid  14178  2cshwcom  14180  2cshwcshw  14189  cshwcshid  14191  cshwcsh2id  14192  s1co  14197  cshco  14200  trclub  14360  shftfval  14431  seqshft  14446  crim  14476  caubnd  14720  limsuplt  14838  isercolllem2  15024  fsumcvg  15071  fsumcvg2  15086  fsumshftm  15138  fsumo1  15169  isumshft  15196  harmonic  15216  cvgrat  15241  mertenslem1  15242  zprod  15293  fprodmodd  15353  bpolylem  15404  bpolysum  15409  bpolydiflem  15410  fsumkthpow  15412  rpnnen2lem12  15580  dvdsval3  15613  negdvdsb  15628  dvdsnegb  15629  dvdsmul1  15633  dvdsabseq  15665  dvdsssfz1  15670  odd2np1  15692  divalglem8  15753  ndvdsadd  15763  dfgcd2  15896  dvdssqim  15906  nn0seqcvgd  15916  seq1st  15917  algcvgblem  15923  lcmf  15979  lcmfunsnlem2  15986  cncongr2  16014  prmdvdsfz  16051  isprm7  16054  prmndvdsfaclt  16069  powm2modprm  16142  modprm0  16144  modprmn0modprm0  16146  pythagtriplem1  16155  pythagtriplem4  16158  pythagtriplem8  16162  pythagtriplem9  16163  pythagtriplem12  16165  pythagtriplem14  16167  pythagtriplem16  16169  pcexp  16198  pc2dvds  16217  pcz  16219  fldivp1  16235  pcfac  16237  oddprmdvds  16241  pockthg  16244  infpnlem1  16248  prmreclem1  16254  prmreclem2  16255  1arith  16265  4sqlem11  16293  vdwlem2  16320  vdwlem8  16326  vdwnnlem2  16334  prmgaplem7  16395  prmgaplem8  16396  cshwshashlem2  16432  cshwshashlem3  16433  pwsval  16761  isacs1i  16930  funcsetcestrclem9  17415  ismgmid  17877  mhmpropd  17964  smndex1gid  18070  smndex1id  18078  grpsubid1  18186  mulgnnp1  18238  mulgsubcl  18244  mulgnn0z  18256  mulgnndir  18258  mulgneg2  18263  lagsubg  18344  ghmco  18380  symg2bas  18523  symgextfv  18548  pgpfi2  18733  efgsfo  18867  frgpupf  18901  frgpup1  18903  gsummptshft  19058  telgsumfzslem  19110  telgsums  19115  ablfac1eu  19197  pgpfac1lem2  19199  ablfaclem3  19211  dvdsrid  19403  dvdsrneg  19406  dvr1  19441  abv1  19606  lmodfopne  19674  lbsexg  19938  gsummoncoe1  20474  xrsds  20590  znf1o  20700  lindfmm  20973  matecl  21036  mavmul0g  21164  gsummatr01  21270  mp2pm2mplem4  21419  chfacfisf  21464  chfacfisfcpmat  21465  chfacfpmmulgsum2  21475  cpmadugsumlemF  21486  isclo  21697  resttopon  21771  restcld  21782  restcls  21791  iscn  21845  iscnp  21847  cnco  21876  cndis  21901  cnindis  21902  cmpsub  22010  hauscmplem  22016  cmpfii  22019  ptcnplem  22231  txtube  22250  txcmplem1  22251  xkoptsub  22264  qtoptop  22310  kqfval  22333  hmeoco  22382  fileln0  22460  trfil1  22496  trfil2  22497  trufil  22520  elfm3  22560  hausflf2  22608  isucn  22889  bl2in  23012  metss2lem  23123  metss2  23124  stdbdxmet  23127  metrest  23136  nmfval2  23202  nmval2  23203  nmoix  23340  ioo2bl  23403  xrsxmet  23419  expcn  23482  elcncf  23499  icccvx  23556  cphsscph  23856  iscmet3  23898  causs  23903  metcld2  23912  metsscmetcld  23920  cncmet  23927  bcth3  23936  ovolgelb  24083  ovolfi  24097  shft2rab  24111  uniioombllem3  24188  dyadmax  24201  dyadmbl  24203  subopnmbl  24207  volcn  24209  mbfid  24238  mbfeqalem2  24245  mbfres  24247  cnmbf  24262  i1fmulc  24306  mbfi1fseqlem3  24320  mbfi1fseqlem4  24321  itg2seq  24345  itg2gt0  24363  itgss3  24417  dvexp  24552  plypow  24797  plyeq0lem  24802  coeidlem  24829  dgrlt  24858  dgrcolem2  24866  elqaalem2  24911  aacjcl  24918  aaliou3lem1  24933  aaliou3lem2  24934  pserdvlem2  25018  abelthlem8  25029  cosord  25118  sinord  25120  resinf1o  25122  relogexp  25181  logdivlt  25206  advlogexp  25240  logcxp  25254  cxpcl  25259  rpcxpcl  25261  cxpne0  25262  logbchbase  25351  logbgt0b  25373  birthdaylem2  25532  cxplim  25551  divsqrtsumo1  25563  zetacvg  25594  wilthlem1  25647  ftalem7  25658  basellem1  25660  issqf  25715  sqf11  25718  sgmf  25724  sgmnncl  25726  sqff1o  25761  dvdsflsumcom  25767  dvdsmulf1o  25773  sgmppw  25775  chtublem  25789  chtub  25790  logexprlim  25803  bposlem3  25864  bposlem5  25866  bposlem6  25867  lgsdirnn0  25922  gausslemma2dlem1a  25943  gausslemma2dlem5a  25948  lgsquad2  25964  lgsquad3  25965  2sqreulem1  26024  2sqreunnlem1  26027  dchrisumlem1  26067  dchrisumlem2  26068  dchrisumlem3  26069  mulogsumlem  26109  brbtwn  26687  uspgrupgrushgr  26964  usgrumgruspgr  26967  cusgrfilem2  27240  finsumvtxdg2ssteplem2  27330  crctcshwlkn0lem4  27593  crctcshwlkn0lem6  27595  crctcshwlkn0lem7  27596  crctcshwlkn0  27601  elwspths2spth  27748  rusgrnumwwlk  27756  clwlkclwwlklem2fv2  27776  erclwwlknref  27850  1to2vfriswmgr  28060  4cycl2v2nb  28070  frgr2wwlkeqm  28112  nvo00  28540  nmorepnf  28547  ubthlem1  28649  normpyc  28925  occon3  29076  pjpreeq  29177  idcnop  29760  riesz3i  29841  cnlnssadj  29859  rnbra  29886  strlem3a  30031  cvcon3  30063  ssdmd1  30092  ssdmd2  30093  relfi  30354  fzsplit3  30519  prmsimpcyc  30858  esumcst  31324  dmvlsiga  31390  ballotlemimin  31765  bnj545  32169  bnj929  32210  bnj953  32213  pthhashvtx  32376  derangsn  32419  iscvm  32508  cvmsval  32515  cvmliftlem7  32540  cvmlift2lem12  32563  mclsssvlem  32811  supfz  32962  faclimlem3  32979  noextenddif  33177  opnrebl2  33671  nn0prpwlem  33672  tailval  33723  nndivlub  33808  ctbssinf  34689  finixpnum  34879  ltflcei  34882  lindsdom  34888  lindsenlbs  34889  matunitlindflem2  34891  poimirlem4  34898  poimirlem14  34908  poimirlem15  34909  poimirlem19  34913  poimirlem20  34914  poimirlem22  34916  poimirlem24  34918  poimirlem28  34922  poimirlem30  34924  poimirlem31  34925  mblfinlem2  34932  mblfinlem3  34933  mblfinlem4  34934  ftc1anclem1  34969  ftc1anclem4  34972  ftc1anclem5  34973  ftc1anclem7  34975  ftc1anclem8  34976  ftc1anc  34977  caushft  35038  ismtyval  35080  heiborlem7  35097  heiborlem10  35100  heibor  35101  oexpreposd  39186  elrfirn  39299  ismrc  39305  nacsfix  39316  mzpcompact2lem  39355  eldiophb  39361  ellz1  39371  rexrabdioph  39398  congrep  39577  jm2.26a  39604  rngunsnply  39780  mendring  39799  iocmbl  39826  rp-isfinite5  39890  enrelmap  40350  expgrowthi  40672  cnfex  41292  xlimclim2lem  42127  climxlim2  42134  icccncfext  42177  itgsinexp  42247  iblspltprt  42265  itgspltprt  42271  fourierdlem50  42448  fourierswlem  42522  etransclem35  42561  zm1nn  43509  subsubelfzo0  43533  iccpartres  43585  iccelpart  43600  iccpartiun  43601  iccpartnel  43605  goldbachthlem1  43714  goldbachth  43716  odz2prm2pw  43732  2pwp1prm  43758  evenltle  43889  fpprwpprb  43912  sbgoldbaltlem2  43952  bgoldbachlt  43985  isomushgr  43998  isomuspgrlem1  43999  isomgrtr  44011  upgrwlkupwlk  44022  mgmhmpropd  44059  2zrngamgm  44217  lincresunit3  44543  lincreslvec3  44544  isldepslvec2  44547  m1modmmod  44588  blengt1fldiv2p1  44660  dignn0flhalf  44685  nn0sumshdiglemA  44686  rrx2pnedifcoorneor  44710  aacllem  44909