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  5572  ordintdif  6403  funco  6575  resdif  6838  fvcofneq  7082  fnprb  7199  fntpb  7200  fvf1pr  7299  isotr  7328  weisoeq  7347  brrpssg  7717  findsg  7891  coexg  7923  resf1extb  7928  xpexgALT  7978  fnsuppres  8188  wfrlem10OLD  8330  oaass  8571  oeword  8600  oeworde  8603  mapsnd  8898  ixpssmapg  8940  enrefnn  9059  pw2f1olem  9088  domsdomtr  9124  xpen  9152  mapen  9153  mapdom1  9154  phplem2  9217  mapfienlem1  9415  elfir  9425  wdomen2  9589  carden2b  9979  harcard  9990  isinffi  10004  acnlem  10060  acndom  10063  alephdom  10093  fin23lem21  10351  fin23lem39  10362  isf32lem5  10369  fin1a2lem12  10423  axdc3lem2  10463  ttukeylem1  10521  pwcfsdom  10595  canthp1  10666  nqereu  10941  addpqf  10956  axmulf  11158  axmulass  11169  axdistr  11170  ltaddnegr  11450  negeu  11470  fimaxre3  12186  nnsub  12282  nn0sub  12549  ltsubnn0  12550  elz2  12604  uzaddcl  12918  qaddcl  12979  xltneg  13231  xleneg  13232  supxrbnd1  13335  infxrgelb  13350  iccneg  13487  uzsubsubfz  13561  fzsplit2  13564  fzadd2  13574  fzss1  13578  uzsplit  13611  fzdif1  13620  fz0fzdiffz0  13652  difelfzle  13656  difelfznle  13657  fvffz0  13661  preduz  13665  predfz  13668  fzonlt0  13697  fzouzsplit  13709  fzo0addelr  13733  eluzgtdifelfzo  13741  elfzodifsumelfzo  13745  ssfzo12  13773  elfznelfzob  13787  fllt  13821  flflp1  13822  uzsup  13878  negmod  13932  modifeq2int  13949  modfzo0difsn  13959  modsumfzodifsn  13960  om2uzlt2i  13967  nn0ennn  13995  suppssfz  14010  seqfveq2  14040  sermono  14050  seqf1o  14059  ser1const  14074  rpexpmord  14184  mulsubdivbinom2  14278  faclbnd  14306  bcval4  14323  bcpasc  14337  hashkf  14348  hashunx  14402  fz1isolem  14477  ishashinf  14479  seqcoll  14480  ccatval1  14593  ccatval21sw  14601  ccatrn  14605  ccatalpha  14609  swrdnd0  14673  swrd0  14674  swrdfv2  14677  swrdspsleq  14681  addlenpfx  14707  ccatpfx  14717  swrdswrd  14721  pfxccatin12lem2  14747  pfxccat3  14750  swrdccat  14751  revccat  14782  repswswrd  14800  cshwmodn  14811  cshwidxmod  14819  repswcshw  14828  2cshwid  14830  2cshwcom  14832  2cshwcshw  14842  cshwcshid  14844  cshwcsh2id  14845  s1co  14850  cshco  14853  trclub  15015  shftfval  15087  seqshft  15102  crim  15132  caubnd  15375  limsuplt  15493  isercolllem2  15680  fsumcvg  15726  fsumcvg2  15741  fsumshftm  15795  fsumo1  15826  isumshft  15853  harmonic  15873  cvgrat  15897  mertenslem1  15898  zprod  15951  fprodmodd  16011  bpolylem  16062  bpolysum  16067  bpolydiflem  16068  fsumkthpow  16070  rpnnen2lem12  16241  dvdsval3  16274  negdvdsb  16290  dvdsnegb  16291  dvdsmul1  16295  dvdsabseq  16330  dvdsssfz1  16335  odd2np1  16358  divalglem8  16417  ndvdsadd  16427  dfgcd2  16563  dvdssqim  16571  nn0seqcvgd  16587  seq1st  16588  algcvgblem  16594  lcmf  16650  lcmfunsnlem2  16657  cncongr2  16685  prmdvdsfz  16722  isprm7  16725  prmndvdsfaclt  16742  powm2modprm  16821  modprm0  16823  modprmn0modprm0  16825  pythagtriplem1  16834  pythagtriplem4  16837  pythagtriplem8  16841  pythagtriplem9  16842  pythagtriplem12  16844  pythagtriplem14  16846  pythagtriplem16  16848  pcexp  16877  pc2dvds  16897  pcz  16899  fldivp1  16915  pcfac  16917  oddprmdvds  16921  pockthg  16924  infpnlem1  16928  prmreclem1  16934  prmreclem2  16935  1arith  16945  4sqlem11  16973  vdwlem2  17000  vdwlem8  17006  vdwnnlem2  17014  prmgaplem7  17075  prmgaplem8  17076  cshwshashlem2  17114  cshwshashlem3  17115  pwsval  17498  isacs1i  17667  funcsetcestrclem9  18173  ismgmid  18641  mgmhmpropd  18674  mhmpropd  18768  smndex1gid  18879  smndex1id  18887  grpsubid1  19006  mulgnnp1  19063  mulgsubcl  19069  mulgnn0z  19082  mulgnndir  19084  mulgneg2  19089  lagsubg  19176  ghmco  19217  symg2bas  19372  symgextfv  19397  pgpfi2  19585  efgsfo  19718  frgpupf  19752  frgpup1  19754  gsummptshft  19915  telgsumfzslem  19967  telgsums  19972  ablfac1eu  20054  pgpfac1lem2  20056  ablfaclem3  20068  dvdsrid  20325  dvdsrneg  20328  dvr1  20365  abv1  20783  lmodfopne  20855  lbsexg  21123  xrsds  21375  znf1o  21510  lindfmm  21785  gsummoncoe1  22244  matecl  22361  mavmul0g  22489  gsummatr01  22595  mp2pm2mplem4  22745  chfacfisf  22790  chfacfisfcpmat  22791  chfacfpmmulgsum2  22801  cpmadugsumlemF  22812  isclo  23023  resttopon  23097  restcld  23108  restcls  23117  iscn  23171  iscnp  23173  cnco  23202  cndis  23227  cnindis  23228  cmpsub  23336  hauscmplem  23342  cmpfii  23345  ptcnplem  23557  txtube  23576  txcmplem1  23577  xkoptsub  23590  qtoptop  23636  kqfval  23659  hmeoco  23708  fileln0  23786  trfil1  23822  trfil2  23823  trufil  23846  elfm3  23886  hausflf2  23934  isucn  24214  bl2in  24337  metss2lem  24448  metss2  24449  stdbdxmet  24452  metrest  24461  nmval2  24529  nmoix  24666  ioo2bl  24730  xrsxmet  24747  expcn  24812  expcnOLD  24814  elcncf  24831  icccvx  24897  cphsscph  25201  iscmet3  25243  causs  25248  metcld2  25257  metsscmetcld  25265  cncmet  25272  bcth3  25281  ovolgelb  25431  ovolfi  25445  shft2rab  25459  uniioombllem3  25536  dyadmax  25549  dyadmbl  25551  subopnmbl  25555  volcn  25557  mbfid  25586  mbfeqalem2  25593  mbfres  25595  cnmbf  25610  i1fmulc  25654  mbfi1fseqlem3  25668  mbfi1fseqlem4  25669  itg2seq  25693  itg2gt0  25711  itgss3  25766  dvexp  25907  plypow  26160  plyeq0lem  26165  coeidlem  26192  dgrlt  26222  dgrcolem2  26230  elqaalem2  26278  aacjcl  26285  aaliou3lem1  26300  aaliou3lem2  26301  pserdvlem2  26388  abelthlem8  26399  cosord  26490  sinord  26493  resinf1o  26495  relogexp  26555  logdivlt  26580  advlogexp  26614  logcxp  26628  cxpcl  26633  rpcxpcl  26635  cxpne0  26636  logbchbase  26731  logbgt0b  26753  birthdaylem2  26912  cxplim  26932  divsqrtsumo1  26944  zetacvg  26975  wilthlem1  27028  ftalem7  27039  basellem1  27041  issqf  27096  sqf11  27099  sgmf  27105  sgmnncl  27107  sqff1o  27142  dvdsflsumcom  27148  mpodvdsmulf1o  27154  dvdsmulf1o  27156  sgmppw  27158  chtublem  27172  chtub  27173  logexprlim  27186  bposlem3  27247  bposlem5  27249  bposlem6  27250  lgsdirnn0  27305  gausslemma2dlem1a  27326  gausslemma2dlem5a  27331  lgsquad2  27347  lgsquad3  27348  2sqreulem1  27407  2sqreunnlem1  27410  dchrisumlem1  27450  dchrisumlem2  27451  dchrisumlem3  27452  mulogsumlem  27492  noextenddif  27630  addsrid  27914  sltneg  27994  sleneg  27995  om2noseqlt2  28223  elzn0s  28301  eln0zs  28303  peano5uzs  28307  brbtwn  28824  uspgrupgrushgr  29104  usgrumgruspgr  29107  cusgrfilem2  29382  finsumvtxdg2ssteplem2  29472  cyclnumvtx  29728  crctcshwlkn0lem4  29741  crctcshwlkn0lem6  29743  crctcshwlkn0lem7  29744  crctcshwlkn0  29749  elwspths2spth  29895  rusgrnumwwlk  29903  clwlkclwwlklem2fv2  29923  erclwwlknref  29996  1to2vfriswmgr  30206  4cycl2v2nb  30216  frgr2wwlkeqm  30258  nvo00  30688  nmorepnf  30695  ubthlem1  30797  normpyc  31073  occon3  31224  pjpreeq  31325  idcnop  31908  riesz3i  31989  cnlnssadj  32007  rnbra  32034  strlem3a  32179  cvcon3  32211  ssdmd1  32240  ssdmd2  32241  relfi  32529  fzsplit3  32716  prmsimpcyc  33171  esumcst  34040  dmvlsiga  34106  ballotlemimin  34484  bnj545  34872  bnj929  34913  bnj953  34916  pthhashvtx  35096  derangsn  35138  iscvm  35227  cvmsval  35234  cvmliftlem7  35259  cvmlift2lem12  35282  mclsssvlem  35530  supfz  35692  faclimlem3  35708  opnrebl2  36285  nn0prpwlem  36286  tailval  36337  nndivlub  36422  ctbssinf  37370  finixpnum  37575  ltflcei  37578  lindsdom  37584  lindsenlbs  37585  matunitlindflem2  37587  poimirlem4  37594  poimirlem14  37604  poimirlem15  37605  poimirlem19  37609  poimirlem20  37610  poimirlem22  37612  poimirlem24  37614  poimirlem28  37618  poimirlem30  37620  poimirlem31  37621  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  ftc1anclem1  37663  ftc1anclem4  37666  ftc1anclem5  37667  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  caushft  37731  ismtyval  37770  heiborlem7  37787  heiborlem10  37790  heibor  37791  lcmineqlem8  41995  deg1gprod  42099  f1o2d2  42231  oexpreposd  42318  elrfirn  42665  ismrc  42671  nacsfix  42682  mzpcompact2lem  42721  eldiophb  42727  ellz1  42737  rexrabdioph  42764  congrep  42944  jm2.26a  42971  rngunsnply  43140  mendring  43159  iocmbl  43184  oeord2lim  43280  cantnfresb  43295  omabs2  43303  ofoafg  43325  dfno2  43399  rp-isfinite5  43488  enrelmap  43968  expgrowthi  44305  cnfex  45000  xlimclim2lem  45816  climxlim2  45823  icccncfext  45864  itgsinexp  45932  iblspltprt  45950  itgspltprt  45956  fourierdlem50  46133  fourierswlem  46207  etransclem35  46246  zm1nn  47279  subsubelfzo0  47303  ceilbi  47310  addmodne  47321  iccpartres  47380  iccelpart  47395  iccpartiun  47396  iccpartnel  47400  goldbachthlem1  47507  goldbachth  47509  odz2prm2pw  47525  2pwp1prm  47551  evenltle  47679  fpprwpprb  47702  sbgoldbaltlem2  47742  bgoldbachlt  47775  isubgredg  47827  gricushgr  47878  uhgrimisgrgriclem  47891  gpgvtx0  48005  gpg5nbgrvtx13starlem2  48022  upgrwlkupwlk  48063  2zrngamgm  48168  lincresunit3  48405  lincreslvec3  48406  isldepslvec2  48409  m1modmmod  48449  blengt1fldiv2p1  48521  dignn0flhalf  48546  nn0sumshdiglemA  48547  rrx2pnedifcoorneor  48644  precofval2  49228  aacllem  49613