Theorem syl2anr 609

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  swopo  5569  ordintdif  6414  funco  6580  resdif  6846  fvcofneq  7093  fnprb  7214  fntpb  7215  fvf1pr  7315  isotr  7344  weisoeq  7365  brrpssg  7741  findsg  7909  coexg  7941  resf1extb  7946  xpexgALT  7993  mpof1o2d  8137  fnsuppres  8209  oaass  8570  oeword  8600  oeworde  8603  mapsnd  8915  ixpssmapg  8957  enrefnn  9075  pw2f1olem  9101  domsdomtr  9132  xpen  9160  mapen  9161  mapdom1  9162  phplem2  9221  mapfienlem1  9398  elfir  9408  wdomen2  9572  carden2b  10049  harcard  10060  isinffi  10074  acnlem  10128  acndom  10131  alephdom  10161  fin23lem21  10418  fin23lem39  10429  isf32lem5  10436  fin1a2lem12  10490  axdc3lem2  10530  ttukeylem1  10588  pwcfsdom  10669  canthp1  10740  nqereu  11015  addpqf  11030  axmulf  11232  axmulass  11243  axdistr  11244  ltaddnegr  11528  negeu  11548  fimaxre3  12264  nnsub  12383  nn0sub  12657  ltsubnn0  12658  elz2  12712  uzaddcl  13032  qaddcl  13094  xltneg  13348  xleneg  13349  supxrbnd1  13452  infxrgelb  13467  iccneg  13604  uzsubsubfz  13681  fzsplit2  13684  fzadd2  13694  fzss1  13698  uzsplit  13731  fzdif1  13740  fz0fzdiffz0  13772  difelfzle  13776  difelfznle  13777  fvffz0  13781  preduz  13785  predfz  13788  fzonlt0  13818  fzouzsplit  13830  fzo0addelr  13855  eluzgtdifelfzo  13863  elfzodifsumelfzo  13867  ssfzo12  13895  elfznelfzob  13910  fllt  13947  flflp1  13948  uzsup  14004  negmod  14060  modifeq2int  14077  modfzo0difsn  14087  modsumfzodifsn  14088  om2uzlt2i  14095  nn0ennn  14123  suppssfz  14138  seqfveq2  14168  sermono  14178  seqf1o  14187  ser1const  14202  rpexpmord  14312  mulsubdivbinom2  14407  faclbnd  14435  bcval4  14452  bcpasc  14466  hashkf  14477  hashunx  14531  fz1isolem  14607  ishashinf  14609  seqcoll  14610  ccatval1  14723  ccatval21sw  14732  ccatrn  14736  ccatalpha  14741  swrdnd0  14808  swrd0  14809  swrdfv2  14812  swrdspsleq  14816  addlenpfx  14841  ccatpfx  14851  swrdswrd  14855  pfxccatin12lem2  14881  pfxccat3  14884  swrdccat  14885  revccat  14916  repswswrd  14936  cshwmodn  14947  cshwidxmod  14955  repswcshw  14964  2cshwid  14966  2cshwcom  14968  2cshwcshw  14977  cshwcshid  14979  cshwcsh2id  14980  s1co  14985  cshco  14988  trclub  15152  shftfval  15224  seqshft  15239  crim  15283  caubnd  15527  limsuplt  15647  isercolllem2  15834  fsumcvg  15879  fsumcvg2  15894  fsumshftm  15948  fsumo1  15980  isumshft  16009  harmonic  16029  cvgrat  16053  mertenslem1  16054  zprod  16105  fprodmodd  16165  bpolylem  16215  bpolysum  16220  bpolydiflem  16221  fsumkthpow  16223  rpnnen2lem12  16394  dvdsval3  16427  negdvdsb  16443  dvdsnegb  16444  dvdsmul1  16448  dvdsabseq  16484  dvdsssfz1  16489  odd2np1  16512  divalglem8  16571  ndvdsadd  16581  dfgcd2  16720  dvdssqim  16728  nn0seqcvgd  16746  seq1st  16747  algcvgblem  16753  lcmf  16809  lcmfunsnlem2  16816  cncongr2  16844  prmdvdsfz  16882  isprm7  16885  prmndvdsfaclt  16902  powm2modprm  16982  modprm0  16984  modprmn0modprm0  16986  pythagtriplem1  16995  pythagtriplem4  16998  pythagtriplem8  17002  pythagtriplem9  17003  pythagtriplem12  17005  pythagtriplem14  17007  pythagtriplem16  17009  pcexp  17038  pc2dvds  17058  pcz  17060  fldivp1  17076  pcfac  17078  oddprmdvds  17082  pockthg  17085  infpnlem1  17089  prmreclem1  17095  prmreclem2  17096  1arith  17106  4sqlem11  17134  vdwlem2  17161  vdwlem8  17167  vdwnnlem2  17175  prmgaplem7  17236  prmgaplem8  17237  cshwshashlem2  17275  cshwshashlem3  17276  pwsval  17658  isacs1i  17832  funcsetcestrclem9  18338  ismgmid  18846  mgmhmpropd  18888  mhmpropd  18988  smndex1gid  19101  smndex1gidOLD  19102  smndex1id  19111  grpsubid1  19236  mulgnnp1  19293  mulgsubcl  19299  mulgnn0z  19312  mulgnndir  19314  mulgneg2  19319  lagsubg  19411  ghmco  19451  symg2bas  19608  symgextfv  19633  pgpfi2  19821  efgsfo  19954  frgpupf  19988  frgpup1  19990  gsummptshft  20151  telgsumfzslem  20203  telgsums  20208  ablfac1eu  20290  pgpfac1lem2  20292  ablfaclem3  20304  dvdsrid  20598  dvdsrneg  20601  dvr1  20638  abv1  21083  lmodfopne  21176  lbsexg  21443  xrsds  21717  znf1o  21858  lindfmm  22134  lindsdom  22157  lindsenlbs  22158  gsummoncoe1  22627  matecl  22741  mavmul0g  22869  gsummatr01  22975  matunitlindflem2  22996  mp2pm2mplem4  23128  chfacfisf  23173  chfacfisfcpmat  23174  chfacfpmmulgsum2  23184  cpmadugsumlemF  23195  isclo  23406  resttopon  23480  restcld  23491  restcls  23500  iscn  23554  iscnp  23556  cnco  23585  cndis  23610  cnindis  23611  cmpsub  23719  hauscmplem  23725  cmpfii  23728  ptcnplem  23941  txtube  23960  txcmplem1  23961  xkoptsub  23974  qtoptop  24020  kqfval  24043  hmeoco  24092  fileln0  24170  trfil1  24206  trfil2  24207  trufil  24230  elfm3  24270  hausflf2  24318  isucn  24597  bl2in  24720  metss2lem  24831  metss2  24832  stdbdxmet  24835  metrest  24844  nmval2  24912  nmoix  25049  ioo2bl  25113  xrsxmet  25130  expcn  25194  elcncf  25211  icccvx  25272  cphsscph  25573  iscmet3  25615  causs  25620  metcld2  25629  metsscmetcld  25637  cncmet  25644  bcth3  25653  ovolgelb  25802  ovolfi  25816  shft2rab  25830  uniioombllem3  25907  dyadmax  25920  dyadmbl  25922  subopnmbl  25926  volcn  25928  mbfid  25957  mbfeqalem2  25964  mbfres  25966  cnmbf  25981  i1fmulc  26025  mbfi1fseqlem3  26039  mbfi1fseqlem4  26040  itg2seq  26064  itg2gt0  26082  itgss3  26136  dvexp  26274  plypow  26524  plyeq0lem  26530  coeidlem  26557  dgrlt  26586  dgrcolem2  26594  elqaalem2  26644  aacjcl  26655  aaliou3lem1  26670  aaliou3lem2  26671  pserdvlem2  26756  abelthlem8  26767  cosord  26860  sinord  26863  resinf1o  26865  relogexp  26925  logdivlt  26950  advlogexp  26984  logcxp  26998  cxpcl  27003  rpcxpcl  27005  cxpne0  27006  logbchbase  27100  logbgt0b  27122  birthdaylem2  27281  cxplim  27300  divsqrtsumo1  27312  zetacvg  27343  wilthlem1  27396  ftalem7  27407  basellem1  27409  issqf  27464  sqf11  27467  sgmf  27473  sgmnncl  27475  sqff1o  27510  dvdsflsumcom  27516  mpodvdsmulf1o  27522  dvdsmulf1o  27524  sgmppw  27525  chtublem  27539  chtub  27540  logexprlim  27553  bposlem3  27614  bposlem5  27616  bposlem6  27617  lgsdirnn0  27672  gausslemma2dlem1a  27693  gausslemma2dlem5a  27698  lgsquad2  27714  lgsquad3  27715  2sqreulem1  27774  2sqreunnlem1  27777  dchrisumlem1  27817  dchrisumlem2  27818  dchrisumlem3  27819  mulogsumlem  27859  fltoprm  27996  noextenddif  28026  addsrid  28351  ltnegs  28432  lenegs  28433  om2noseqlt2  28687  elzn0s  28785  eln0zs  28787  peano5uzs  28791  bdayfinbndlem1  28854  brbtwn  29478  uspgrupgrushgr  29761  usgrumgruspgr  29764  cusgrfilem2  30038  finsumvtxdg2ssteplem2  30128  pthhashvtx  30316  cyclnumvtx  30389  crctcshwlkn0lem4  30403  crctcshwlkn0lem6  30405  crctcshwlkn0lem7  30406  crctcshwlkn0  30411  elwspths2spth  30560  rusgrnumwwlk  30568  clwlkclwwlklem2fv2  30588  erclwwlknref  30661  1to2vfriswmgr  30881  4cycl2v2nb  30891  frgr2wwlkeqm  30933  nvo00  31364  nmorepnf  31371  ubthlem1  31473  normpyc  31749  occon3  31900  pjpreeq  32001  idcnop  32584  riesz3i  32665  cnlnssadj  32683  rnbra  32710  strlem3a  32855  cvcon3  32887  ssdmd1  32916  ssdmd2  32917  relfi  33239  fcobijfs2  33357  fzsplit3  33428  prmsimpcyc  33832  esumcst  34738  dmvlsiga  34804  ballotlemimin  35181  bnj545  35568  bnj929  35609  bnj953  35612  fineqvnttrclselem1  35838  derangsn  36004  iscvm  36093  cvmsval  36100  cvmliftlem7  36125  cvmlift2lem12  36148  mclsssvlem  36396  supfz  36569  faclimlem3  36585  opnrebl2  37184  nn0prpwlem  37185  tailval  37236  nndivlub  37321  ctbssinf  38405  finixpnum  38604  ltflcei  38607  poimirlem4  38618  poimirlem14  38628  poimirlem15  38629  poimirlem19  38633  poimirlem20  38634  poimirlem22  38636  poimirlem24  38638  poimirlem28  38642  poimirlem30  38644  poimirlem31  38645  mblfinlem2  38652  mblfinlem3  38653  mblfinlem4  38654  ftc1anclem1  38687  ftc1anclem4  38690  ftc1anclem5  38691  ftc1anclem7  38693  ftc1anclem8  38694  ftc1anc  38695  caushft  38771  ismtyval  38810  heiborlem7  38827  heiborlem10  38830  heibor  38831  lcmineqlem8  43162  deg1gprod  43266  oexpreposd  43455  elrfirn  43782  ismrc  43788  nacsfix  43799  mzpcompact2lem  43838  eldiophb  43844  ellz1  43854  rexrabdioph  43877  congrep  44056  jm2.26a  44083  rngunsnply  44247  mendring  44266  iocmbl  44291  oeord2lim  44387  cantnfresb  44402  omabs2  44410  ofoafg  44432  dfno2  44505  rp-isfinite5  44594  enrelmap  45073  expgrowthi  45393  hashnnltb  46089  cnfex  46121  xlimclim2lem  46925  climxlim2  46932  icccncfext  46973  itgsinexp  47041  iblspltprt  47059  itgspltprt  47065  fourierdlem50  47242  fourierswlem  47316  etransclem35  47355  zm1nn  48448  subsubelfzo0  48473  ceilbi  48483  addmodne  48496  m1modmmod  48510  modlt0b  48515  iccpartres  48576  iccelpart  48591  iccpartiun  48592  iccpartnel  48596  nprmmul1  48685  goldbachthlem1  48706  goldbachth  48708  odz2prm2pw  48724  2pwp1prm  48750  evenltle  48891  fpprwpprb  48914  sbgoldbaltlem2  48954  bgoldbachlt  48987  isubgredg  49040  gricushgr  49091  uhgrimisgrgriclem  49104  gpgvtx0  49227  gpg5nbgrvtx13starlem2  49246  upgrwlkupwlk  49314  2zrngamgm  49418  lincresunit3  49669  lincreslvec3  49670  isldepslvec2  49673  blengt1fldiv2p1  49781  dignn0flhalf  49806  nn0sumshdiglemA  49807  rrx2pnedifcoorneor  49904  precofval2  50553  aacllem  51015