Theorem syl2anr 608

Description: A double syllogism inference. For an implication-only version, see syl2imc 42. (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 607	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
5	4	ancoms 463	1 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  swopo  5580  ordintdif  6412  funco  6576  resdif  6842  fvcofneq  7088  fnprb  7206  fntpb  7207  fvf1pr  7305  isotr  7334  weisoeq  7353  brrpssg  7722  findsg  7893  coexg  7925  resf1extb  7930  xpexgALT  7977  mpof1o2d  8120  fnsuppres  8186  oaass  8545  oeword  8575  oeworde  8578  mapsnd  8883  ixpssmapg  8925  enrefnn  9042  pw2f1olem  9068  domsdomtr  9099  xpen  9127  mapen  9128  mapdom1  9129  phplem2  9188  mapfienlem1  9364  elfir  9374  wdomen2  9538  carden2b  9952  harcard  9963  isinffi  9977  acnlem  10031  acndom  10034  alephdom  10064  fin23lem21  10322  fin23lem39  10333  isf32lem5  10340  fin1a2lem12  10394  axdc3lem2  10434  ttukeylem1  10492  pwcfsdom  10567  canthp1  10638  nqereu  10913  addpqf  10928  axmulf  11130  axmulass  11141  axdistr  11142  ltaddnegr  11426  negeu  11446  fimaxre3  12160  nnsub  12279  nn0sub  12553  ltsubnn0  12554  elz2  12608  uzaddcl  12927  qaddcl  12988  xltneg  13242  xleneg  13243  supxrbnd1  13346  infxrgelb  13361  iccneg  13498  uzsubsubfz  13574  fzsplit2  13577  fzadd2  13587  fzss1  13591  uzsplit  13624  fzdif1  13633  fz0fzdiffz0  13665  difelfzle  13669  difelfznle  13670  fvffz0  13674  preduz  13678  predfz  13681  fzonlt0  13711  fzouzsplit  13723  fzo0addelr  13748  eluzgtdifelfzo  13756  elfzodifsumelfzo  13760  ssfzo12  13788  elfznelfzob  13803  fllt  13839  flflp1  13840  uzsup  13896  negmod  13952  modifeq2int  13969  modfzo0difsn  13979  modsumfzodifsn  13980  om2uzlt2i  13987  nn0ennn  14015  suppssfz  14030  seqfveq2  14060  sermono  14070  seqf1o  14079  ser1const  14094  rpexpmord  14204  mulsubdivbinom2  14298  faclbnd  14326  bcval4  14343  bcpasc  14357  hashkf  14368  hashunx  14422  fz1isolem  14498  ishashinf  14500  seqcoll  14501  ccatval1  14614  ccatval21sw  14623  ccatrn  14627  ccatalpha  14631  swrdnd0  14695  swrd0  14696  swrdfv2  14699  swrdspsleq  14703  addlenpfx  14728  ccatpfx  14738  swrdswrd  14742  pfxccatin12lem2  14768  pfxccat3  14771  swrdccat  14772  revccat  14803  repswswrd  14821  cshwmodn  14832  cshwidxmod  14840  repswcshw  14849  2cshwid  14851  2cshwcom  14853  2cshwcshw  14862  cshwcshid  14864  cshwcsh2id  14865  s1co  14870  cshco  14873  trclub  15035  shftfval  15107  seqshft  15122  crim  15166  caubnd  15410  limsuplt  15530  isercolllem2  15717  fsumcvg  15763  fsumcvg2  15778  fsumshftm  15832  fsumo1  15864  isumshft  15893  harmonic  15913  cvgrat  15937  mertenslem1  15938  zprod  15991  fprodmodd  16051  bpolylem  16101  bpolysum  16106  bpolydiflem  16107  fsumkthpow  16109  rpnnen2lem12  16280  dvdsval3  16313  negdvdsb  16329  dvdsnegb  16330  dvdsmul1  16334  dvdsabseq  16370  dvdsssfz1  16375  odd2np1  16398  divalglem8  16457  ndvdsadd  16467  dfgcd2  16603  dvdssqim  16611  nn0seqcvgd  16627  seq1st  16628  algcvgblem  16634  lcmf  16690  lcmfunsnlem2  16697  cncongr2  16725  prmdvdsfz  16763  isprm7  16766  prmndvdsfaclt  16783  powm2modprm  16862  modprm0  16864  modprmn0modprm0  16866  pythagtriplem1  16875  pythagtriplem4  16878  pythagtriplem8  16882  pythagtriplem9  16883  pythagtriplem12  16885  pythagtriplem14  16887  pythagtriplem16  16889  pcexp  16918  pc2dvds  16938  pcz  16940  fldivp1  16956  pcfac  16958  oddprmdvds  16962  pockthg  16965  infpnlem1  16969  prmreclem1  16975  prmreclem2  16976  1arith  16986  4sqlem11  17014  vdwlem2  17041  vdwlem8  17047  vdwnnlem2  17055  prmgaplem7  17116  prmgaplem8  17117  cshwshashlem2  17155  cshwshashlem3  17156  pwsval  17538  isacs1i  17712  funcsetcestrclem9  18218  ismgmid  18722  mgmhmpropd  18755  mhmpropd  18849  smndex1gid  18962  smndex1gidOLD  18963  smndex1id  18972  grpsubid1  19090  mulgnnp1  19147  mulgsubcl  19153  mulgnn0z  19166  mulgnndir  19168  mulgneg2  19173  lagsubg  19265  ghmco  19305  symg2bas  19462  symgextfv  19487  pgpfi2  19675  efgsfo  19808  frgpupf  19842  frgpup1  19844  gsummptshft  20005  telgsumfzslem  20057  telgsums  20062  ablfac1eu  20144  pgpfac1lem2  20146  ablfaclem3  20158  dvdsrid  20448  dvdsrneg  20451  dvr1  20488  abv1  20907  lmodfopne  21000  lbsexg  21267  xrsds  21539  znf1o  21680  lindfmm  21956  gsummoncoe1  22447  matecl  22561  mavmul0g  22689  gsummatr01  22795  mp2pm2mplem4  22945  chfacfisf  22990  chfacfisfcpmat  22991  chfacfpmmulgsum2  23001  cpmadugsumlemF  23012  isclo  23223  resttopon  23297  restcld  23308  restcls  23317  iscn  23371  iscnp  23373  cnco  23402  cndis  23427  cnindis  23428  cmpsub  23536  hauscmplem  23542  cmpfii  23545  ptcnplem  23757  txtube  23776  txcmplem1  23777  xkoptsub  23790  qtoptop  23836  kqfval  23859  hmeoco  23908  fileln0  23986  trfil1  24022  trfil2  24023  trufil  24046  elfm3  24086  hausflf2  24134  isucn  24413  bl2in  24536  metss2lem  24647  metss2  24648  stdbdxmet  24651  metrest  24660  nmval2  24728  nmoix  24865  ioo2bl  24929  xrsxmet  24946  expcn  25010  elcncf  25027  icccvx  25088  cphsscph  25389  iscmet3  25431  causs  25436  metcld2  25445  metsscmetcld  25453  cncmet  25460  bcth3  25469  ovolgelb  25618  ovolfi  25632  shft2rab  25646  uniioombllem3  25723  dyadmax  25736  dyadmbl  25738  subopnmbl  25742  volcn  25744  mbfid  25773  mbfeqalem2  25780  mbfres  25782  cnmbf  25797  i1fmulc  25841  mbfi1fseqlem3  25855  mbfi1fseqlem4  25856  itg2seq  25880  itg2gt0  25898  itgss3  25953  dvexp  26091  plypow  26341  plyeq0lem  26346  coeidlem  26373  dgrlt  26402  dgrcolem2  26410  elqaalem2  26460  aacjcl  26467  aaliou3lem1  26482  aaliou3lem2  26483  pserdvlem2  26567  abelthlem8  26578  cosord  26672  sinord  26675  resinf1o  26677  relogexp  26737  logdivlt  26762  advlogexp  26796  logcxp  26810  cxpcl  26815  rpcxpcl  26817  cxpne0  26818  logbchbase  26912  logbgt0b  26934  birthdaylem2  27093  cxplim  27112  divsqrtsumo1  27124  zetacvg  27155  wilthlem1  27208  ftalem7  27219  basellem1  27221  issqf  27276  sqf11  27279  sgmf  27285  sgmnncl  27287  sqff1o  27322  dvdsflsumcom  27328  mpodvdsmulf1o  27334  dvdsmulf1o  27336  sgmppw  27337  chtublem  27351  chtub  27352  logexprlim  27365  bposlem3  27426  bposlem5  27428  bposlem6  27429  lgsdirnn0  27484  gausslemma2dlem1a  27505  gausslemma2dlem5a  27510  lgsquad2  27526  lgsquad3  27527  2sqreulem1  27586  2sqreunnlem1  27589  dchrisumlem1  27629  dchrisumlem2  27630  dchrisumlem3  27631  mulogsumlem  27671  noextenddif  27808  addsrid  28133  ltnegs  28214  lenegs  28215  om2noseqlt2  28469  elzn0s  28567  eln0zs  28569  peano5uzs  28573  bdayfinbndlem1  28636  brbtwn  29215  uspgrupgrushgr  29495  usgrumgruspgr  29498  cusgrfilem2  29772  finsumvtxdg2ssteplem2  29862  cyclnumvtx  30115  crctcshwlkn0lem4  30128  crctcshwlkn0lem6  30130  crctcshwlkn0lem7  30131  crctcshwlkn0  30136  elwspths2spth  30285  rusgrnumwwlk  30293  clwlkclwwlklem2fv2  30313  erclwwlknref  30386  1to2vfriswmgr  30596  4cycl2v2nb  30606  frgr2wwlkeqm  30648  nvo00  31079  nmorepnf  31086  ubthlem1  31188  normpyc  31464  occon3  31615  pjpreeq  31716  idcnop  32299  riesz3i  32380  cnlnssadj  32398  rnbra  32425  strlem3a  32570  cvcon3  32602  ssdmd1  32631  ssdmd2  32632  relfi  32913  fcobijfs2  33033  fzsplit3  33104  prmsimpcyc  33514  esumcst  34419  dmvlsiga  34485  ballotlemimin  34862  bnj545  35249  bnj929  35290  bnj953  35293  fineqvnttrclselem1  35500  pthhashvtx  35586  derangsn  35628  iscvm  35717  cvmsval  35724  cvmliftlem7  35749  cvmlift2lem12  35772  mclsssvlem  36020  supfz  36187  faclimlem3  36203  opnrebl2  36798  nn0prpwlem  36799  tailval  36850  nndivlub  36935  ctbssinf  38018  finixpnum  38222  ltflcei  38225  lindsdom  38231  lindsenlbs  38232  matunitlindflem2  38234  poimirlem4  38241  poimirlem14  38251  poimirlem15  38252  poimirlem19  38256  poimirlem20  38257  poimirlem22  38259  poimirlem24  38261  poimirlem28  38265  poimirlem30  38267  poimirlem31  38268  mblfinlem2  38275  mblfinlem3  38276  mblfinlem4  38277  ftc1anclem1  38310  ftc1anclem4  38313  ftc1anclem5  38314  ftc1anclem7  38316  ftc1anclem8  38317  ftc1anc  38318  caushft  38378  ismtyval  38417  heiborlem7  38434  heiborlem10  38437  heibor  38438  lcmineqlem8  42771  deg1gprod  42875  oexpreposd  43051  elrfirn  43396  ismrc  43402  nacsfix  43413  mzpcompact2lem  43452  eldiophb  43458  ellz1  43468  rexrabdioph  43491  congrep  43670  jm2.26a  43697  rngunsnply  43866  mendring  43885  iocmbl  43910  oeord2lim  44006  cantnfresb  44021  omabs2  44029  ofoafg  44051  dfno2  44124  rp-isfinite5  44213  enrelmap  44693  expgrowthi  45013  hashnnltb  45702  cnfex  45718  xlimclim2lem  46523  climxlim2  46530  icccncfext  46571  itgsinexp  46639  iblspltprt  46657  itgspltprt  46663  fourierdlem50  46840  fourierswlem  46914  etransclem35  46953  zm1nn  48006  subsubelfzo0  48031  ceilbi  48041  addmodne  48054  m1modmmod  48068  modlt0b  48073  iccpartres  48134  iccelpart  48149  iccpartiun  48150  iccpartnel  48154  nprmmul1  48243  goldbachthlem1  48264  goldbachth  48266  odz2prm2pw  48282  2pwp1prm  48308  evenltle  48449  fpprwpprb  48472  sbgoldbaltlem2  48512  bgoldbachlt  48545  isubgredg  48598  gricushgr  48649  uhgrimisgrgriclem  48662  gpgvtx0  48785  gpg5nbgrvtx13starlem2  48804  upgrwlkupwlk  48872  2zrngamgm  48977  lincresunit3  49228  lincreslvec3  49229  isldepslvec2  49232  blengt1fldiv2p1  49340  dignn0flhalf  49365  nn0sumshdiglemA  49366  rrx2pnedifcoorneor  49463  precofval2  50114  aacllem  50568