Theorem syl2anr 597

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  swopo  5560  ordintdif  6386  funco  6559  resdif  6824  fvcofneq  7068  fnprb  7185  fntpb  7186  fvf1pr  7285  isotr  7314  weisoeq  7333  brrpssg  7704  findsg  7876  coexg  7908  resf1extb  7913  xpexgALT  7963  fnsuppres  8173  oaass  8528  oeword  8557  oeworde  8560  mapsnd  8862  ixpssmapg  8904  enrefnn  9021  pw2f1olem  9050  domsdomtr  9082  xpen  9110  mapen  9111  mapdom1  9112  phplem2  9175  mapfienlem1  9363  elfir  9373  wdomen2  9537  carden2b  9927  harcard  9938  isinffi  9952  acnlem  10008  acndom  10011  alephdom  10041  fin23lem21  10299  fin23lem39  10310  isf32lem5  10317  fin1a2lem12  10371  axdc3lem2  10411  ttukeylem1  10469  pwcfsdom  10543  canthp1  10614  nqereu  10889  addpqf  10904  axmulf  11106  axmulass  11117  axdistr  11118  ltaddnegr  11398  negeu  11418  fimaxre3  12136  nnsub  12237  nn0sub  12499  ltsubnn0  12500  elz2  12554  uzaddcl  12870  qaddcl  12931  xltneg  13184  xleneg  13185  supxrbnd1  13288  infxrgelb  13303  iccneg  13440  uzsubsubfz  13514  fzsplit2  13517  fzadd2  13527  fzss1  13531  uzsplit  13564  fzdif1  13573  fz0fzdiffz0  13605  difelfzle  13609  difelfznle  13610  fvffz0  13614  preduz  13618  predfz  13621  fzonlt0  13650  fzouzsplit  13662  fzo0addelr  13687  eluzgtdifelfzo  13695  elfzodifsumelfzo  13699  ssfzo12  13727  elfznelfzob  13741  fllt  13775  flflp1  13776  uzsup  13832  negmod  13888  modifeq2int  13905  modfzo0difsn  13915  modsumfzodifsn  13916  om2uzlt2i  13923  nn0ennn  13951  suppssfz  13966  seqfveq2  13996  sermono  14006  seqf1o  14015  ser1const  14030  rpexpmord  14140  mulsubdivbinom2  14234  faclbnd  14262  bcval4  14279  bcpasc  14293  hashkf  14304  hashunx  14358  fz1isolem  14433  ishashinf  14435  seqcoll  14436  ccatval1  14549  ccatval21sw  14557  ccatrn  14561  ccatalpha  14565  swrdnd0  14629  swrd0  14630  swrdfv2  14633  swrdspsleq  14637  addlenpfx  14663  ccatpfx  14673  swrdswrd  14677  pfxccatin12lem2  14703  pfxccat3  14706  swrdccat  14707  revccat  14738  repswswrd  14756  cshwmodn  14767  cshwidxmod  14775  repswcshw  14784  2cshwid  14786  2cshwcom  14788  2cshwcshw  14798  cshwcshid  14800  cshwcsh2id  14801  s1co  14806  cshco  14809  trclub  14971  shftfval  15043  seqshft  15058  crim  15088  caubnd  15332  limsuplt  15452  isercolllem2  15639  fsumcvg  15685  fsumcvg2  15700  fsumshftm  15754  fsumo1  15785  isumshft  15812  harmonic  15832  cvgrat  15856  mertenslem1  15857  zprod  15910  fprodmodd  15970  bpolylem  16021  bpolysum  16026  bpolydiflem  16027  fsumkthpow  16029  rpnnen2lem12  16200  dvdsval3  16233  negdvdsb  16249  dvdsnegb  16250  dvdsmul1  16254  dvdsabseq  16290  dvdsssfz1  16295  odd2np1  16318  divalglem8  16377  ndvdsadd  16387  dfgcd2  16523  dvdssqim  16531  nn0seqcvgd  16547  seq1st  16548  algcvgblem  16554  lcmf  16610  lcmfunsnlem2  16617  cncongr2  16645  prmdvdsfz  16682  isprm7  16685  prmndvdsfaclt  16702  powm2modprm  16781  modprm0  16783  modprmn0modprm0  16785  pythagtriplem1  16794  pythagtriplem4  16797  pythagtriplem8  16801  pythagtriplem9  16802  pythagtriplem12  16804  pythagtriplem14  16806  pythagtriplem16  16808  pcexp  16837  pc2dvds  16857  pcz  16859  fldivp1  16875  pcfac  16877  oddprmdvds  16881  pockthg  16884  infpnlem1  16888  prmreclem1  16894  prmreclem2  16895  1arith  16905  4sqlem11  16933  vdwlem2  16960  vdwlem8  16966  vdwnnlem2  16974  prmgaplem7  17035  prmgaplem8  17036  cshwshashlem2  17074  cshwshashlem3  17075  pwsval  17456  isacs1i  17625  funcsetcestrclem9  18131  ismgmid  18599  mgmhmpropd  18632  mhmpropd  18726  smndex1gid  18837  smndex1id  18845  grpsubid1  18964  mulgnnp1  19021  mulgsubcl  19027  mulgnn0z  19040  mulgnndir  19042  mulgneg2  19047  lagsubg  19134  ghmco  19175  symg2bas  19330  symgextfv  19355  pgpfi2  19543  efgsfo  19676  frgpupf  19710  frgpup1  19712  gsummptshft  19873  telgsumfzslem  19925  telgsums  19930  ablfac1eu  20012  pgpfac1lem2  20014  ablfaclem3  20026  dvdsrid  20283  dvdsrneg  20286  dvr1  20323  abv1  20741  lmodfopne  20813  lbsexg  21081  xrsds  21333  znf1o  21468  lindfmm  21743  gsummoncoe1  22202  matecl  22319  mavmul0g  22447  gsummatr01  22553  mp2pm2mplem4  22703  chfacfisf  22748  chfacfisfcpmat  22749  chfacfpmmulgsum2  22759  cpmadugsumlemF  22770  isclo  22981  resttopon  23055  restcld  23066  restcls  23075  iscn  23129  iscnp  23131  cnco  23160  cndis  23185  cnindis  23186  cmpsub  23294  hauscmplem  23300  cmpfii  23303  ptcnplem  23515  txtube  23534  txcmplem1  23535  xkoptsub  23548  qtoptop  23594  kqfval  23617  hmeoco  23666  fileln0  23744  trfil1  23780  trfil2  23781  trufil  23804  elfm3  23844  hausflf2  23892  isucn  24172  bl2in  24295  metss2lem  24406  metss2  24407  stdbdxmet  24410  metrest  24419  nmval2  24487  nmoix  24624  ioo2bl  24688  xrsxmet  24705  expcn  24770  expcnOLD  24772  elcncf  24789  icccvx  24855  cphsscph  25158  iscmet3  25200  causs  25205  metcld2  25214  metsscmetcld  25222  cncmet  25229  bcth3  25238  ovolgelb  25388  ovolfi  25402  shft2rab  25416  uniioombllem3  25493  dyadmax  25506  dyadmbl  25508  subopnmbl  25512  volcn  25514  mbfid  25543  mbfeqalem2  25550  mbfres  25552  cnmbf  25567  i1fmulc  25611  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  itg2seq  25650  itg2gt0  25668  itgss3  25723  dvexp  25864  plypow  26117  plyeq0lem  26122  coeidlem  26149  dgrlt  26179  dgrcolem2  26187  elqaalem2  26235  aacjcl  26242  aaliou3lem1  26257  aaliou3lem2  26258  pserdvlem2  26345  abelthlem8  26356  cosord  26447  sinord  26450  resinf1o  26452  relogexp  26512  logdivlt  26537  advlogexp  26571  logcxp  26585  cxpcl  26590  rpcxpcl  26592  cxpne0  26593  logbchbase  26688  logbgt0b  26710  birthdaylem2  26869  cxplim  26889  divsqrtsumo1  26901  zetacvg  26932  wilthlem1  26985  ftalem7  26996  basellem1  26998  issqf  27053  sqf11  27056  sgmf  27062  sgmnncl  27064  sqff1o  27099  dvdsflsumcom  27105  mpodvdsmulf1o  27111  dvdsmulf1o  27113  sgmppw  27115  chtublem  27129  chtub  27130  logexprlim  27143  bposlem3  27204  bposlem5  27206  bposlem6  27207  lgsdirnn0  27262  gausslemma2dlem1a  27283  gausslemma2dlem5a  27288  lgsquad2  27304  lgsquad3  27305  2sqreulem1  27364  2sqreunnlem1  27367  dchrisumlem1  27407  dchrisumlem2  27408  dchrisumlem3  27409  mulogsumlem  27449  noextenddif  27587  addsrid  27878  sltneg  27958  sleneg  27959  om2noseqlt2  28201  elzn0s  28293  eln0zs  28295  peano5uzs  28299  brbtwn  28833  uspgrupgrushgr  29113  usgrumgruspgr  29116  cusgrfilem2  29391  finsumvtxdg2ssteplem2  29481  cyclnumvtx  29737  crctcshwlkn0lem4  29750  crctcshwlkn0lem6  29752  crctcshwlkn0lem7  29753  crctcshwlkn0  29758  elwspths2spth  29904  rusgrnumwwlk  29912  clwlkclwwlklem2fv2  29932  erclwwlknref  30005  1to2vfriswmgr  30215  4cycl2v2nb  30225  frgr2wwlkeqm  30267  nvo00  30697  nmorepnf  30704  ubthlem1  30806  normpyc  31082  occon3  31233  pjpreeq  31334  idcnop  31917  riesz3i  31998  cnlnssadj  32016  rnbra  32043  strlem3a  32188  cvcon3  32220  ssdmd1  32249  ssdmd2  32250  relfi  32538  fzsplit3  32723  prmsimpcyc  33188  esumcst  34060  dmvlsiga  34126  ballotlemimin  34504  bnj545  34892  bnj929  34933  bnj953  34936  pthhashvtx  35122  derangsn  35164  iscvm  35253  cvmsval  35260  cvmliftlem7  35285  cvmlift2lem12  35308  mclsssvlem  35556  supfz  35723  faclimlem3  35739  opnrebl2  36316  nn0prpwlem  36317  tailval  36368  nndivlub  36453  ctbssinf  37401  finixpnum  37606  ltflcei  37609  lindsdom  37615  lindsenlbs  37616  matunitlindflem2  37618  poimirlem4  37625  poimirlem14  37635  poimirlem15  37636  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  poimirlem24  37645  poimirlem28  37649  poimirlem30  37651  poimirlem31  37652  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  ftc1anclem1  37694  ftc1anclem4  37697  ftc1anclem5  37698  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  caushft  37762  ismtyval  37801  heiborlem7  37818  heiborlem10  37821  heibor  37822  lcmineqlem8  42031  deg1gprod  42135  f1o2d2  42228  oexpreposd  42317  elrfirn  42690  ismrc  42696  nacsfix  42707  mzpcompact2lem  42746  eldiophb  42752  ellz1  42762  rexrabdioph  42789  congrep  42969  jm2.26a  42996  rngunsnply  43165  mendring  43184  iocmbl  43209  oeord2lim  43305  cantnfresb  43320  omabs2  43328  ofoafg  43350  dfno2  43424  rp-isfinite5  43513  enrelmap  43993  expgrowthi  44329  cnfex  45029  xlimclim2lem  45844  climxlim2  45851  icccncfext  45892  itgsinexp  45960  iblspltprt  45978  itgspltprt  45984  fourierdlem50  46161  fourierswlem  46235  etransclem35  46274  zm1nn  47307  subsubelfzo0  47331  ceilbi  47338  addmodne  47349  m1modmmod  47363  modlt0b  47368  iccpartres  47423  iccelpart  47438  iccpartiun  47439  iccpartnel  47443  goldbachthlem1  47550  goldbachth  47552  odz2prm2pw  47568  2pwp1prm  47594  evenltle  47722  fpprwpprb  47745  sbgoldbaltlem2  47785  bgoldbachlt  47818  isubgredg  47870  gricushgr  47921  uhgrimisgrgriclem  47934  gpgvtx0  48048  gpg5nbgrvtx13starlem2  48067  upgrwlkupwlk  48132  2zrngamgm  48237  lincresunit3  48474  lincreslvec3  48475  isldepslvec2  48478  blengt1fldiv2p1  48586  dignn0flhalf  48611  nn0sumshdiglemA  48612  rrx2pnedifcoorneor  48709  precofval2  49362  aacllem  49794