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 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  5619  ordintdif  6445  funco  6618  resdif  6883  fvcofneq  7127  fnprb  7245  fntpb  7246  fvf1pr  7343  isotr  7372  weisoeq  7391  brrpssg  7760  findsg  7937  coexg  7969  xpexgALT  8022  fnsuppres  8232  wfrlem10OLD  8374  oaass  8617  oeword  8646  oeworde  8649  mapsnd  8944  ixpssmapg  8986  enrefnn  9113  pw2f1olem  9142  domsdomtr  9178  xpen  9206  mapen  9207  mapdom1  9208  phplem2  9271  mapfienlem1  9474  elfir  9484  wdomen2  9646  carden2b  10036  harcard  10047  isinffi  10061  acnlem  10117  acndom  10120  alephdom  10150  fin23lem21  10408  fin23lem39  10419  isf32lem5  10426  fin1a2lem12  10480  axdc3lem2  10520  ttukeylem1  10578  pwcfsdom  10652  canthp1  10723  nqereu  10998  addpqf  11013  axmulf  11215  axmulass  11226  axdistr  11227  ltaddnegr  11506  negeu  11526  fimaxre3  12241  nnsub  12337  nn0sub  12603  ltsubnn0  12604  elz2  12657  uzaddcl  12969  qaddcl  13030  xltneg  13279  xleneg  13280  supxrbnd1  13383  infxrgelb  13397  iccneg  13532  uzsubsubfz  13606  fzsplit2  13609  fzadd2  13619  fzss1  13623  uzsplit  13656  fz0fzdiffz0  13694  difelfzle  13698  difelfznle  13699  fvffz0  13703  preduz  13707  predfz  13710  fzonlt0  13739  fzouzsplit  13751  fzo0addelr  13771  eluzgtdifelfzo  13778  elfzodifsumelfzo  13782  ssfzo12  13809  elfznelfzob  13823  fllt  13857  flflp1  13858  uzsup  13914  negmod  13967  modifeq2int  13984  modfzo0difsn  13994  modsumfzodifsn  13995  om2uzlt2i  14002  nn0ennn  14030  suppssfz  14045  seqfveq2  14075  sermono  14085  seqf1o  14094  ser1const  14109  rpexpmord  14218  mulsubdivbinom2  14311  faclbnd  14339  bcval4  14356  bcpasc  14370  hashkf  14381  hashunx  14435  fz1isolem  14510  ishashinf  14512  seqcoll  14513  ccatval1  14625  ccatval21sw  14633  ccatrn  14637  ccatalpha  14641  swrdnd0  14705  swrd0  14706  swrdfv2  14709  swrdspsleq  14713  addlenpfx  14739  ccatpfx  14749  swrdswrd  14753  pfxccatin12lem2  14779  pfxccat3  14782  swrdccat  14783  revccat  14814  repswswrd  14832  cshwmodn  14843  cshwidxmod  14851  repswcshw  14860  2cshwid  14862  2cshwcom  14864  2cshwcshw  14874  cshwcshid  14876  cshwcsh2id  14877  s1co  14882  cshco  14885  trclub  15047  shftfval  15119  seqshft  15134  crim  15164  caubnd  15407  limsuplt  15525  isercolllem2  15714  fsumcvg  15760  fsumcvg2  15775  fsumshftm  15829  fsumo1  15860  isumshft  15887  harmonic  15907  cvgrat  15931  mertenslem1  15932  zprod  15985  fprodmodd  16045  bpolylem  16096  bpolysum  16101  bpolydiflem  16102  fsumkthpow  16104  rpnnen2lem12  16273  dvdsval3  16306  negdvdsb  16321  dvdsnegb  16322  dvdsmul1  16326  dvdsabseq  16361  dvdsssfz1  16366  odd2np1  16389  divalglem8  16448  ndvdsadd  16458  dfgcd2  16593  dvdssqim  16601  nn0seqcvgd  16617  seq1st  16618  algcvgblem  16624  lcmf  16680  lcmfunsnlem2  16687  cncongr2  16715  prmdvdsfz  16752  isprm7  16755  prmndvdsfaclt  16772  powm2modprm  16850  modprm0  16852  modprmn0modprm0  16854  pythagtriplem1  16863  pythagtriplem4  16866  pythagtriplem8  16870  pythagtriplem9  16871  pythagtriplem12  16873  pythagtriplem14  16875  pythagtriplem16  16877  pcexp  16906  pc2dvds  16926  pcz  16928  fldivp1  16944  pcfac  16946  oddprmdvds  16950  pockthg  16953  infpnlem1  16957  prmreclem1  16963  prmreclem2  16964  1arith  16974  4sqlem11  17002  vdwlem2  17029  vdwlem8  17035  vdwnnlem2  17043  prmgaplem7  17104  prmgaplem8  17105  cshwshashlem2  17144  cshwshashlem3  17145  pwsval  17546  isacs1i  17715  funcsetcestrclem9  18232  ismgmid  18703  mgmhmpropd  18736  mhmpropd  18827  smndex1gid  18938  smndex1id  18946  grpsubid1  19065  mulgnnp1  19122  mulgsubcl  19128  mulgnn0z  19141  mulgnndir  19143  mulgneg2  19148  lagsubg  19235  ghmco  19276  symg2bas  19434  symgextfv  19460  pgpfi2  19648  efgsfo  19781  frgpupf  19815  frgpup1  19817  gsummptshft  19978  telgsumfzslem  20030  telgsums  20035  ablfac1eu  20117  pgpfac1lem2  20119  ablfaclem3  20131  dvdsrid  20393  dvdsrneg  20396  dvr1  20433  abv1  20848  lmodfopne  20920  lbsexg  21189  xrsds  21450  znf1o  21593  lindfmm  21870  gsummoncoe1  22333  matecl  22452  mavmul0g  22580  gsummatr01  22686  mp2pm2mplem4  22836  chfacfisf  22881  chfacfisfcpmat  22882  chfacfpmmulgsum2  22892  cpmadugsumlemF  22903  isclo  23116  resttopon  23190  restcld  23201  restcls  23210  iscn  23264  iscnp  23266  cnco  23295  cndis  23320  cnindis  23321  cmpsub  23429  hauscmplem  23435  cmpfii  23438  ptcnplem  23650  txtube  23669  txcmplem1  23670  xkoptsub  23683  qtoptop  23729  kqfval  23752  hmeoco  23801  fileln0  23879  trfil1  23915  trfil2  23916  trufil  23939  elfm3  23979  hausflf2  24027  isucn  24308  bl2in  24431  metss2lem  24545  metss2  24546  stdbdxmet  24549  metrest  24558  nmval2  24626  nmoix  24771  ioo2bl  24834  xrsxmet  24850  expcn  24915  expcnOLD  24917  elcncf  24934  icccvx  25000  cphsscph  25304  iscmet3  25346  causs  25351  metcld2  25360  metsscmetcld  25368  cncmet  25375  bcth3  25384  ovolgelb  25534  ovolfi  25548  shft2rab  25562  uniioombllem3  25639  dyadmax  25652  dyadmbl  25654  subopnmbl  25658  volcn  25660  mbfid  25689  mbfeqalem2  25696  mbfres  25698  cnmbf  25713  i1fmulc  25758  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  itg2seq  25797  itg2gt0  25815  itgss3  25870  dvexp  26011  plypow  26264  plyeq0lem  26269  coeidlem  26296  dgrlt  26326  dgrcolem2  26334  elqaalem2  26380  aacjcl  26387  aaliou3lem1  26402  aaliou3lem2  26403  pserdvlem2  26490  abelthlem8  26501  cosord  26591  sinord  26594  resinf1o  26596  relogexp  26656  logdivlt  26681  advlogexp  26715  logcxp  26729  cxpcl  26734  rpcxpcl  26736  cxpne0  26737  logbchbase  26832  logbgt0b  26854  birthdaylem2  27013  cxplim  27033  divsqrtsumo1  27045  zetacvg  27076  wilthlem1  27129  ftalem7  27140  basellem1  27142  issqf  27197  sqf11  27200  sgmf  27206  sgmnncl  27208  sqff1o  27243  dvdsflsumcom  27249  mpodvdsmulf1o  27255  dvdsmulf1o  27257  sgmppw  27259  chtublem  27273  chtub  27274  logexprlim  27287  bposlem3  27348  bposlem5  27350  bposlem6  27351  lgsdirnn0  27406  gausslemma2dlem1a  27427  gausslemma2dlem5a  27432  lgsquad2  27448  lgsquad3  27449  2sqreulem1  27508  2sqreunnlem1  27511  dchrisumlem1  27551  dchrisumlem2  27552  dchrisumlem3  27553  mulogsumlem  27593  noextenddif  27731  addsrid  28015  sltneg  28095  sleneg  28096  om2noseqlt2  28324  elzn0s  28402  eln0zs  28404  peano5uzs  28408  brbtwn  28932  uspgrupgrushgr  29214  usgrumgruspgr  29217  cusgrfilem2  29492  finsumvtxdg2ssteplem2  29582  crctcshwlkn0lem4  29846  crctcshwlkn0lem6  29848  crctcshwlkn0lem7  29849  crctcshwlkn0  29854  elwspths2spth  30000  rusgrnumwwlk  30008  clwlkclwwlklem2fv2  30028  erclwwlknref  30101  1to2vfriswmgr  30311  4cycl2v2nb  30321  frgr2wwlkeqm  30363  nvo00  30793  nmorepnf  30800  ubthlem1  30902  normpyc  31178  occon3  31329  pjpreeq  31430  idcnop  32013  riesz3i  32094  cnlnssadj  32112  rnbra  32139  strlem3a  32284  cvcon3  32316  ssdmd1  32345  ssdmd2  32346  relfi  32624  fzsplit3  32799  prmsimpcyc  33207  esumcst  34027  dmvlsiga  34093  ballotlemimin  34470  bnj545  34871  bnj929  34912  bnj953  34915  pthhashvtx  35095  derangsn  35138  iscvm  35227  cvmsval  35234  cvmliftlem7  35259  cvmlift2lem12  35282  mclsssvlem  35530  supfz  35691  faclimlem3  35707  opnrebl2  36287  nn0prpwlem  36288  tailval  36339  nndivlub  36424  ctbssinf  37372  finixpnum  37565  ltflcei  37568  lindsdom  37574  lindsenlbs  37575  matunitlindflem2  37577  poimirlem4  37584  poimirlem14  37594  poimirlem15  37595  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  poimirlem24  37604  poimirlem28  37608  poimirlem30  37610  poimirlem31  37611  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  ftc1anclem1  37653  ftc1anclem4  37656  ftc1anclem5  37657  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  caushft  37721  ismtyval  37760  heiborlem7  37777  heiborlem10  37780  heibor  37781  lcmineqlem8  41993  deg1gprod  42097  f1o2d2  42228  oexpreposd  42309  elrfirn  42651  ismrc  42657  nacsfix  42668  mzpcompact2lem  42707  eldiophb  42713  ellz1  42723  rexrabdioph  42750  congrep  42930  jm2.26a  42957  rngunsnply  43130  mendring  43149  iocmbl  43174  oeord2lim  43271  cantnfresb  43286  omabs2  43294  ofoafg  43316  dfno2  43390  rp-isfinite5  43479  enrelmap  43959  expgrowthi  44302  cnfex  44928  xlimclim2lem  45760  climxlim2  45767  icccncfext  45808  itgsinexp  45876  iblspltprt  45894  itgspltprt  45900  fourierdlem50  46077  fourierswlem  46151  etransclem35  46190  zm1nn  47217  subsubelfzo0  47241  iccpartres  47292  iccelpart  47307  iccpartiun  47308  iccpartnel  47312  goldbachthlem1  47419  goldbachth  47421  odz2prm2pw  47437  2pwp1prm  47463  evenltle  47591  fpprwpprb  47614  sbgoldbaltlem2  47654  bgoldbachlt  47687  gricushgr  47770  uhgrimisgrgriclem  47782  upgrwlkupwlk  47863  2zrngamgm  47968  lincresunit3  48210  lincreslvec3  48211  isldepslvec2  48214  m1modmmod  48255  blengt1fldiv2p1  48327  dignn0flhalf  48352  nn0sumshdiglemA  48353  rrx2pnedifcoorneor  48450  aacllem  48895