Theorem syl2anr 596

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 595	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
5	4	ancoms 459	1 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  swopo  5379  ordintdif  6122  funco  6272  resdif  6510  fvcofneq  6731  fnprb  6844  fntpb  6845  isotr  6959  weisoeq  6978  brrpssg  7316  findsg  7472  coexg  7497  xpexgALT  7545  fnsuppres  7715  wfrlem10  7823  oaass  8044  oeword  8073  oeworde  8076  mapsnd  8306  ixpssmapg  8347  pw2f1olem  8475  domsdomtr  8506  xpen  8534  mapen  8535  mapdom1  8536  mapfienlem1  8721  elfir  8732  wdomen2  8894  carden2b  9249  harcard  9260  isinffi  9274  acnlem  9327  acndom  9330  alephdom  9360  fin23lem21  9614  fin23lem39  9625  isf32lem5  9632  fin1a2lem12  9686  axdc3lem2  9726  ttukeylem1  9784  pwcfsdom  9858  canthp1  9929  nqereu  10204  addpqf  10219  axmulf  10421  axmulass  10432  axdistr  10433  ltaddnegr  10709  negeu  10729  fimaxre3  11441  nnsub  11535  nn0sub  11801  ltsubnn0  11802  elz2  11853  uzaddcl  12157  qaddcl  12218  xltneg  12464  xleneg  12465  supxrbnd1  12568  infxrgelb  12582  iccneg  12712  uzsubsubfz  12783  fzsplit2  12786  fzadd2  12796  fzss1  12800  uzsplit  12833  fz0fzdiffz0  12870  difelfzle  12874  difelfznle  12875  fvffz0  12879  preduz  12883  predfz  12886  fzonlt0  12914  fzouzsplit  12926  fzo0addelr  12946  eluzgtdifelfzo  12953  elfzodifsumelfzo  12957  ssfzo12  12984  elfznelfzob  12997  fllt  13030  flflp1  13031  uzsup  13085  negmod  13138  modifeq2int  13155  modfzo0difsn  13165  modsumfzodifsn  13166  om2uzlt2i  13173  nn0ennn  13201  suppssfz  13216  seqfveq2  13246  sermono  13256  seqf1o  13265  ser1const  13280  rpexpmord  13386  mulsubdivbinom2  13476  faclbnd  13504  bcval4  13521  bcpasc  13535  hashkf  13546  hashunx  13599  hashfacen  13664  fz1isolem  13671  ishashinf  13673  seqcoll  13674  ccatval21sw  13787  ccatalpha  13795  swrdnd0  13859  swrd0  13860  swrdfv2  13863  swrdspsleq  13867  addlenpfx  13893  swrdswrd  13907  pfxccatin12lem2  13933  pfxccat3  13936  swrdccat  13937  revccat  13968  repswswrd  13986  cshwmodn  13997  cshwidxmod  14005  repswcshw  14014  2cshwid  14016  2cshwcom  14018  2cshwcshw  14027  cshwcshid  14029  cshwcsh2id  14030  s1co  14035  cshco  14038  trclub  14196  shftfval  14267  seqshft  14282  crim  14312  caubnd  14556  limsuplt  14674  isercolllem2  14860  fsumcvg  14906  fsumcvg2  14921  fsumshftm  14973  fsumo1  15004  isumshft  15031  harmonic  15051  cvgrat  15076  mertenslem1  15077  zprod  15128  fprodmodd  15188  bpolylem  15239  bpolysum  15244  bpolydiflem  15245  fsumkthpow  15247  rpnnen2lem12  15415  dvdsval3  15448  negdvdsb  15463  dvdsnegb  15464  dvdsmul1  15468  dvdsabseq  15500  dvdsssfz1  15505  odd2np1  15527  divalglem8  15588  ndvdsadd  15598  dfgcd2  15727  dvdssqim  15737  nn0seqcvgd  15747  seq1st  15748  algcvgblem  15754  lcmf  15810  lcmfunsnlem2  15817  cncongr2  15845  prmdvdsfz  15882  isprm7  15885  prmndvdsfaclt  15900  powm2modprm  15973  modprm0  15975  modprmn0modprm0  15977  pythagtriplem1  15986  pythagtriplem4  15989  pythagtriplem8  15993  pythagtriplem9  15994  pythagtriplem12  15996  pythagtriplem14  15998  pythagtriplem16  16000  pcexp  16029  pc2dvds  16048  pcz  16050  fldivp1  16066  pcfac  16068  oddprmdvds  16072  pockthg  16075  infpnlem1  16079  prmreclem1  16085  prmreclem2  16086  1arith  16096  4sqlem11  16124  vdwlem2  16151  vdwlem8  16157  vdwnnlem2  16165  prmgaplem7  16226  prmgaplem8  16227  cshwshashlem2  16263  cshwshashlem3  16264  pwsval  16592  isacs1i  16761  funcsetcestrclem9  17246  ismgmid  17707  mhmpropd  17784  grpsubid1  17945  mulgnnp1  17995  mulgsubcl  18001  mulgnn0z  18012  mulgnndir  18014  mulgneg2  18019  lagsubg  18099  ghmco  18123  symg2bas  18261  symgextfv  18281  pgpfi2  18465  efgsfo  18596  frgpupf  18630  frgpup1  18632  gsummptshft  18780  telgsumfzslem  18829  telgsums  18834  ablfac1eu  18916  pgpfac1lem2  18918  ablfaclem3  18930  dvdsrid  19095  dvdsrneg  19098  dvr1  19133  abv1  19298  lmodfopne  19366  lbsexg  19630  gsummoncoe1  20159  xrsds  20274  znf1o  20384  lindfmm  20657  matecl  20722  mavmul0g  20850  gsummatr01  20956  mp2pm2mplem4  21105  chfacfisf  21150  chfacfisfcpmat  21151  chfacfpmmulgsum2  21161  cpmadugsumlemF  21172  isclo  21383  resttopon  21457  restcld  21468  restcls  21477  iscn  21531  iscnp  21533  cnco  21562  cndis  21587  cnindis  21588  cmpsub  21696  hauscmplem  21702  cmpfii  21705  ptcnplem  21917  txtube  21936  txcmplem1  21937  xkoptsub  21950  qtoptop  21996  kqfval  22019  hmeoco  22068  fileln0  22146  trfil1  22182  trfil2  22183  trufil  22206  elfm3  22246  hausflf2  22294  isucn  22574  bl2in  22697  metss2lem  22808  metss2  22809  stdbdxmet  22812  metrest  22821  nmfval2  22887  nmval2  22888  nmoix  23025  ioo2bl  23088  xrsxmet  23104  expcn  23167  elcncf  23184  icccvx  23241  cphsscph  23541  iscmet3  23583  causs  23588  metcld2  23597  metsscmetcld  23605  cncmet  23612  bcth3  23621  ovolgelb  23768  ovolfi  23782  shft2rab  23796  uniioombllem3  23873  dyadmax  23886  dyadmbl  23888  subopnmbl  23892  volcn  23894  mbfid  23923  mbfeqalem2  23930  mbfres  23932  cnmbf  23947  i1fmulc  23991  mbfi1fseqlem3  24005  mbfi1fseqlem4  24006  itg2seq  24030  itg2gt0  24048  itgss3  24102  dvexp  24237  plypow  24482  plyeq0lem  24487  coeidlem  24514  dgrlt  24543  dgrcolem2  24551  elqaalem2  24596  aacjcl  24603  aaliou3lem1  24618  aaliou3lem2  24619  pserdvlem2  24703  abelthlem8  24714  cosord  24801  sinord  24803  resinf1o  24805  relogexp  24864  logdivlt  24889  advlogexp  24923  logcxp  24937  cxpcl  24942  rpcxpcl  24944  cxpne0  24945  logbchbase  25034  logbgt0b  25056  birthdaylem2  25216  cxplim  25235  divsqrtsumo1  25247  zetacvg  25278  wilthlem1  25331  ftalem7  25342  basellem1  25344  issqf  25399  sqf11  25402  sgmf  25408  sgmnncl  25410  sqff1o  25445  dvdsflsumcom  25451  dvdsmulf1o  25457  sgmppw  25459  chtublem  25473  chtub  25474  logexprlim  25487  bposlem3  25548  bposlem5  25550  bposlem6  25551  lgsdirnn0  25606  gausslemma2dlem1a  25627  gausslemma2dlem5a  25632  lgsquad2  25648  lgsquad3  25649  2sqreulem1  25708  2sqreunnlem1  25711  dchrisumlem1  25751  dchrisumlem2  25752  dchrisumlem3  25753  mulogsumlem  25793  brbtwn  26372  uspgrupgrushgr  26649  usgrumgruspgr  26652  cusgrfilem2  26925  finsumvtxdg2ssteplem2  27015  crctcshwlkn0lem4  27277  crctcshwlkn0lem6  27279  crctcshwlkn0lem7  27280  crctcshwlkn0  27285  elwspths2spth  27432  rusgrnumwwlk  27440  clwwlkccatlem  27453  clwlkclwwlklem2fv2  27460  erclwwlknref  27534  clwwlknonex2e  27575  1to2vfriswmgr  27746  4cycl2v2nb  27756  frgr2wwlkeqm  27798  nvo00  28225  nmorepnf  28232  ubthlem1  28334  normpyc  28610  occon3  28761  pjpreeq  28862  idcnop  29445  riesz3i  29526  cnlnssadj  29544  rnbra  29571  strlem3a  29716  cvcon3  29748  ssdmd1  29777  ssdmd2  29778  relfi  30038  fzsplit3  30199  esumcst  30935  dmvlsiga  31001  ballotlemimin  31376  bnj545  31779  bnj929  31820  bnj953  31823  pthhashvtx  31984  derangsn  32027  iscvm  32116  cvmsval  32123  cvmliftlem7  32148  cvmlift2lem12  32171  mclsssvlem  32419  supfz  32570  faclimlem3  32587  noextenddif  32786  opnrebl2  33280  nn0prpwlem  33281  tailval  33332  nndivlub  33417  ctbssinf  34239  finixpnum  34429  ltflcei  34432  lindsdom  34438  lindsenlbs  34439  matunitlindflem2  34441  poimirlem4  34448  poimirlem14  34458  poimirlem15  34459  poimirlem19  34463  poimirlem20  34464  poimirlem22  34466  poimirlem24  34468  poimirlem28  34472  poimirlem30  34474  poimirlem31  34475  mblfinlem2  34482  mblfinlem3  34483  mblfinlem4  34484  ftc1anclem1  34519  ftc1anclem4  34522  ftc1anclem5  34523  ftc1anclem7  34525  ftc1anclem8  34526  ftc1anc  34527  caushft  34589  ismtyval  34631  heiborlem7  34648  heiborlem10  34651  heibor  34652  oexpreposd  38722  elrfirn  38798  ismrc  38804  nacsfix  38815  mzpcompact2lem  38854  eldiophb  38860  ellz1  38870  rexrabdioph  38897  congrep  39076  jm2.26a  39103  rngunsnply  39279  mendring  39298  iocmbl  39325  rp-isfinite5  39389  enrelmap  39849  prmsimpcyc  40195  expgrowthi  40224  cnfex  40845  xlimclim2lem  41683  climxlim2  41690  icccncfext  41733  itgsinexp  41803  iblspltprt  41821  itgspltprt  41827  fourierdlem50  42005  fourierswlem  42079  etransclem35  42118  zm1nn  43040  subsubelfzo0  43064  iccpartres  43082  iccelpart  43097  iccpartiun  43098  iccpartnel  43102  goldbachthlem1  43211  goldbachth  43213  odz2prm2pw  43229  2pwp1prm  43255  evenltle  43386  fpprwpprb  43409  sbgoldbaltlem2  43449  bgoldbachlt  43482  isomushgr  43495  isomuspgrlem1  43496  isomgrtr  43508  upgrwlkupwlk  43519  mgmhmpropd  43556  2zrngamgm  43710  lincresunit3  44038  lincreslvec3  44039  isldepslvec2  44042  m1modmmod  44084  blengt1fldiv2p1  44156  dignn0flhalf  44181  nn0sumshdiglemA  44182  rrx2pnedifcoorneor  44206  aacllem  44404