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  5533  ordintdif  6353  funco  6517  resdif  6780  fvcofneq  7021  fnprb  7137  fntpb  7138  fvf1pr  7236  isotr  7265  weisoeq  7284  brrpssg  7653  findsg  7822  coexg  7854  resf1extb  7859  xpexgALT  7908  fnsuppres  8116  oaass  8471  oeword  8500  oeworde  8503  mapsnd  8805  ixpssmapg  8847  enrefnn  8963  pw2f1olem  8989  domsdomtr  9020  xpen  9048  mapen  9049  mapdom1  9050  phplem2  9109  mapfienlem1  9284  elfir  9294  wdomen2  9458  carden2b  9852  harcard  9863  isinffi  9877  acnlem  9931  acndom  9934  alephdom  9964  fin23lem21  10222  fin23lem39  10233  isf32lem5  10240  fin1a2lem12  10294  axdc3lem2  10334  ttukeylem1  10392  pwcfsdom  10466  canthp1  10537  nqereu  10812  addpqf  10827  axmulf  11029  axmulass  11040  axdistr  11041  ltaddnegr  11322  negeu  11342  fimaxre3  12060  nnsub  12161  nn0sub  12423  ltsubnn0  12424  elz2  12478  uzaddcl  12794  qaddcl  12855  xltneg  13108  xleneg  13109  supxrbnd1  13212  infxrgelb  13227  iccneg  13364  uzsubsubfz  13438  fzsplit2  13441  fzadd2  13451  fzss1  13455  uzsplit  13488  fzdif1  13497  fz0fzdiffz0  13529  difelfzle  13533  difelfznle  13534  fvffz0  13538  preduz  13542  predfz  13545  fzonlt0  13574  fzouzsplit  13586  fzo0addelr  13611  eluzgtdifelfzo  13619  elfzodifsumelfzo  13623  ssfzo12  13651  elfznelfzob  13666  fllt  13702  flflp1  13703  uzsup  13759  negmod  13815  modifeq2int  13832  modfzo0difsn  13842  modsumfzodifsn  13843  om2uzlt2i  13850  nn0ennn  13878  suppssfz  13893  seqfveq2  13923  sermono  13933  seqf1o  13942  ser1const  13957  rpexpmord  14067  mulsubdivbinom2  14161  faclbnd  14189  bcval4  14206  bcpasc  14220  hashkf  14231  hashunx  14285  fz1isolem  14360  ishashinf  14362  seqcoll  14363  ccatval1  14476  ccatval21sw  14485  ccatrn  14489  ccatalpha  14493  swrdnd0  14557  swrd0  14558  swrdfv2  14561  swrdspsleq  14565  addlenpfx  14590  ccatpfx  14600  swrdswrd  14604  pfxccatin12lem2  14630  pfxccat3  14633  swrdccat  14634  revccat  14665  repswswrd  14683  cshwmodn  14694  cshwidxmod  14702  repswcshw  14711  2cshwid  14713  2cshwcom  14715  2cshwcshw  14724  cshwcshid  14726  cshwcsh2id  14727  s1co  14732  cshco  14735  trclub  14897  shftfval  14969  seqshft  14984  crim  15014  caubnd  15258  limsuplt  15378  isercolllem2  15565  fsumcvg  15611  fsumcvg2  15626  fsumshftm  15680  fsumo1  15711  isumshft  15738  harmonic  15758  cvgrat  15782  mertenslem1  15783  zprod  15836  fprodmodd  15896  bpolylem  15947  bpolysum  15952  bpolydiflem  15953  fsumkthpow  15955  rpnnen2lem12  16126  dvdsval3  16159  negdvdsb  16175  dvdsnegb  16176  dvdsmul1  16180  dvdsabseq  16216  dvdsssfz1  16221  odd2np1  16244  divalglem8  16303  ndvdsadd  16313  dfgcd2  16449  dvdssqim  16457  nn0seqcvgd  16473  seq1st  16474  algcvgblem  16480  lcmf  16536  lcmfunsnlem2  16543  cncongr2  16571  prmdvdsfz  16608  isprm7  16611  prmndvdsfaclt  16628  powm2modprm  16707  modprm0  16709  modprmn0modprm0  16711  pythagtriplem1  16720  pythagtriplem4  16723  pythagtriplem8  16727  pythagtriplem9  16728  pythagtriplem12  16730  pythagtriplem14  16732  pythagtriplem16  16734  pcexp  16763  pc2dvds  16783  pcz  16785  fldivp1  16801  pcfac  16803  oddprmdvds  16807  pockthg  16810  infpnlem1  16814  prmreclem1  16820  prmreclem2  16821  1arith  16831  4sqlem11  16859  vdwlem2  16886  vdwlem8  16892  vdwnnlem2  16900  prmgaplem7  16961  prmgaplem8  16962  cshwshashlem2  17000  cshwshashlem3  17001  pwsval  17382  isacs1i  17555  funcsetcestrclem9  18061  ismgmid  18565  mgmhmpropd  18598  mhmpropd  18692  smndex1gid  18803  smndex1id  18811  grpsubid1  18930  mulgnnp1  18987  mulgsubcl  18993  mulgnn0z  19006  mulgnndir  19008  mulgneg2  19013  lagsubg  19100  ghmco  19141  symg2bas  19298  symgextfv  19323  pgpfi2  19511  efgsfo  19644  frgpupf  19678  frgpup1  19680  gsummptshft  19841  telgsumfzslem  19893  telgsums  19898  ablfac1eu  19980  pgpfac1lem2  19982  ablfaclem3  19994  dvdsrid  20278  dvdsrneg  20281  dvr1  20318  abv1  20733  lmodfopne  20826  lbsexg  21094  xrsds  21339  znf1o  21481  lindfmm  21757  gsummoncoe1  22216  matecl  22333  mavmul0g  22461  gsummatr01  22567  mp2pm2mplem4  22717  chfacfisf  22762  chfacfisfcpmat  22763  chfacfpmmulgsum2  22773  cpmadugsumlemF  22784  isclo  22995  resttopon  23069  restcld  23080  restcls  23089  iscn  23143  iscnp  23145  cnco  23174  cndis  23199  cnindis  23200  cmpsub  23308  hauscmplem  23314  cmpfii  23317  ptcnplem  23529  txtube  23548  txcmplem1  23549  xkoptsub  23562  qtoptop  23608  kqfval  23631  hmeoco  23680  fileln0  23758  trfil1  23794  trfil2  23795  trufil  23818  elfm3  23858  hausflf2  23906  isucn  24185  bl2in  24308  metss2lem  24419  metss2  24420  stdbdxmet  24423  metrest  24432  nmval2  24500  nmoix  24637  ioo2bl  24701  xrsxmet  24718  expcn  24783  expcnOLD  24785  elcncf  24802  icccvx  24868  cphsscph  25171  iscmet3  25213  causs  25218  metcld2  25227  metsscmetcld  25235  cncmet  25242  bcth3  25251  ovolgelb  25401  ovolfi  25415  shft2rab  25429  uniioombllem3  25506  dyadmax  25519  dyadmbl  25521  subopnmbl  25525  volcn  25527  mbfid  25556  mbfeqalem2  25563  mbfres  25565  cnmbf  25580  i1fmulc  25624  mbfi1fseqlem3  25638  mbfi1fseqlem4  25639  itg2seq  25663  itg2gt0  25681  itgss3  25736  dvexp  25877  plypow  26130  plyeq0lem  26135  coeidlem  26162  dgrlt  26192  dgrcolem2  26200  elqaalem2  26248  aacjcl  26255  aaliou3lem1  26270  aaliou3lem2  26271  pserdvlem2  26358  abelthlem8  26369  cosord  26460  sinord  26463  resinf1o  26465  relogexp  26525  logdivlt  26550  advlogexp  26584  logcxp  26598  cxpcl  26603  rpcxpcl  26605  cxpne0  26606  logbchbase  26701  logbgt0b  26723  birthdaylem2  26882  cxplim  26902  divsqrtsumo1  26914  zetacvg  26945  wilthlem1  26998  ftalem7  27009  basellem1  27011  issqf  27066  sqf11  27069  sgmf  27075  sgmnncl  27077  sqff1o  27112  dvdsflsumcom  27118  mpodvdsmulf1o  27124  dvdsmulf1o  27126  sgmppw  27128  chtublem  27142  chtub  27143  logexprlim  27156  bposlem3  27217  bposlem5  27219  bposlem6  27220  lgsdirnn0  27275  gausslemma2dlem1a  27296  gausslemma2dlem5a  27301  lgsquad2  27317  lgsquad3  27318  2sqreulem1  27377  2sqreunnlem1  27380  dchrisumlem1  27420  dchrisumlem2  27421  dchrisumlem3  27422  mulogsumlem  27462  noextenddif  27600  addsrid  27900  sltneg  27980  sleneg  27981  om2noseqlt2  28223  elzn0s  28315  eln0zs  28317  peano5uzs  28321  brbtwn  28870  uspgrupgrushgr  29150  usgrumgruspgr  29153  cusgrfilem2  29428  finsumvtxdg2ssteplem2  29518  cyclnumvtx  29771  crctcshwlkn0lem4  29784  crctcshwlkn0lem6  29786  crctcshwlkn0lem7  29787  crctcshwlkn0  29792  elwspths2spth  29938  rusgrnumwwlk  29946  clwlkclwwlklem2fv2  29966  erclwwlknref  30039  1to2vfriswmgr  30249  4cycl2v2nb  30259  frgr2wwlkeqm  30301  nvo00  30731  nmorepnf  30738  ubthlem1  30840  normpyc  31116  occon3  31267  pjpreeq  31368  idcnop  31951  riesz3i  32032  cnlnssadj  32050  rnbra  32077  strlem3a  32222  cvcon3  32254  ssdmd1  32283  ssdmd2  32284  relfi  32572  fcobijfs2  32695  fzsplit3  32766  prmsimpcyc  33187  esumcst  34066  dmvlsiga  34132  ballotlemimin  34509  bnj545  34897  bnj929  34938  bnj953  34941  fineqvnttrclselem1  35109  pthhashvtx  35140  derangsn  35182  iscvm  35271  cvmsval  35278  cvmliftlem7  35303  cvmlift2lem12  35326  mclsssvlem  35574  supfz  35741  faclimlem3  35757  opnrebl2  36334  nn0prpwlem  36335  tailval  36386  nndivlub  36471  ctbssinf  37419  finixpnum  37624  ltflcei  37627  lindsdom  37633  lindsenlbs  37634  matunitlindflem2  37636  poimirlem4  37643  poimirlem14  37653  poimirlem15  37654  poimirlem19  37658  poimirlem20  37659  poimirlem22  37661  poimirlem24  37663  poimirlem28  37667  poimirlem30  37669  poimirlem31  37670  mblfinlem2  37677  mblfinlem3  37678  mblfinlem4  37679  ftc1anclem1  37712  ftc1anclem4  37715  ftc1anclem5  37716  ftc1anclem7  37718  ftc1anclem8  37719  ftc1anc  37720  caushft  37780  ismtyval  37819  heiborlem7  37836  heiborlem10  37839  heibor  37840  lcmineqlem8  42048  deg1gprod  42152  f1o2d2  42245  oexpreposd  42334  elrfirn  42707  ismrc  42713  nacsfix  42724  mzpcompact2lem  42763  eldiophb  42769  ellz1  42779  rexrabdioph  42806  congrep  42985  jm2.26a  43012  rngunsnply  43181  mendring  43200  iocmbl  43225  oeord2lim  43321  cantnfresb  43336  omabs2  43344  ofoafg  43366  dfno2  43440  rp-isfinite5  43529  enrelmap  44009  expgrowthi  44345  cnfex  45044  xlimclim2lem  45856  climxlim2  45863  icccncfext  45904  itgsinexp  45972  iblspltprt  45990  itgspltprt  45996  fourierdlem50  46173  fourierswlem  46247  etransclem35  46286  zm1nn  47312  subsubelfzo0  47336  ceilbi  47343  addmodne  47354  m1modmmod  47368  modlt0b  47373  iccpartres  47428  iccelpart  47443  iccpartiun  47444  iccpartnel  47448  goldbachthlem1  47555  goldbachth  47557  odz2prm2pw  47573  2pwp1prm  47599  evenltle  47727  fpprwpprb  47750  sbgoldbaltlem2  47790  bgoldbachlt  47823  isubgredg  47876  gricushgr  47927  uhgrimisgrgriclem  47940  gpgvtx0  48063  gpg5nbgrvtx13starlem2  48082  upgrwlkupwlk  48150  2zrngamgm  48255  lincresunit3  48492  lincreslvec3  48493  isldepslvec2  48496  blengt1fldiv2p1  48604  dignn0flhalf  48629  nn0sumshdiglemA  48630  rrx2pnedifcoorneor  48727  precofval2  49380  aacllem  49812