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  5566  ordintdif  6403  funco  6568  resdif  6834  fvcofneq  7081  fnprb  7202  fntpb  7203  fvf1pr  7303  isotr  7332  weisoeq  7353  brrpssg  7724  findsg  7892  coexg  7924  resf1extb  7929  xpexgALT  7976  mpof1o2d  8120  fnsuppres  8186  oaass  8547  oeword  8577  oeworde  8580  mapsnd  8892  ixpssmapg  8934  enrefnn  9052  pw2f1olem  9078  domsdomtr  9109  xpen  9137  mapen  9138  mapdom1  9139  phplem2  9198  mapfienlem1  9375  elfir  9385  wdomen2  9549  carden2b  10020  harcard  10031  isinffi  10045  acnlem  10099  acndom  10102  alephdom  10132  fin23lem21  10389  fin23lem39  10400  isf32lem5  10407  fin1a2lem12  10461  axdc3lem2  10501  ttukeylem1  10559  pwcfsdom  10640  canthp1  10711  nqereu  10986  addpqf  11001  axmulf  11203  axmulass  11214  axdistr  11215  ltaddnegr  11499  negeu  11519  fimaxre3  12233  nnsub  12352  nn0sub  12626  ltsubnn0  12627  elz2  12681  uzaddcl  13001  qaddcl  13063  xltneg  13317  xleneg  13318  supxrbnd1  13421  infxrgelb  13436  iccneg  13573  uzsubsubfz  13649  fzsplit2  13652  fzadd2  13662  fzss1  13666  uzsplit  13699  fzdif1  13708  fz0fzdiffz0  13740  difelfzle  13744  difelfznle  13745  fvffz0  13749  preduz  13753  predfz  13756  fzonlt0  13786  fzouzsplit  13798  fzo0addelr  13823  eluzgtdifelfzo  13831  elfzodifsumelfzo  13835  ssfzo12  13863  elfznelfzob  13878  fllt  13915  flflp1  13916  uzsup  13972  negmod  14028  modifeq2int  14045  modfzo0difsn  14055  modsumfzodifsn  14056  om2uzlt2i  14063  nn0ennn  14091  suppssfz  14106  seqfveq2  14136  sermono  14146  seqf1o  14155  ser1const  14170  rpexpmord  14280  mulsubdivbinom2  14374  faclbnd  14402  bcval4  14419  bcpasc  14433  hashkf  14444  hashunx  14498  fz1isolem  14574  ishashinf  14576  seqcoll  14577  ccatval1  14690  ccatval21sw  14699  ccatrn  14703  ccatalpha  14708  swrdnd0  14775  swrd0  14776  swrdfv2  14779  swrdspsleq  14783  addlenpfx  14808  ccatpfx  14818  swrdswrd  14822  pfxccatin12lem2  14848  pfxccat3  14851  swrdccat  14852  revccat  14883  repswswrd  14903  cshwmodn  14914  cshwidxmod  14922  repswcshw  14931  2cshwid  14933  2cshwcom  14935  2cshwcshw  14944  cshwcshid  14946  cshwcsh2id  14947  s1co  14952  cshco  14955  trclub  15119  shftfval  15191  seqshft  15206  crim  15250  caubnd  15494  limsuplt  15614  isercolllem2  15801  fsumcvg  15846  fsumcvg2  15861  fsumshftm  15915  fsumo1  15947  isumshft  15976  harmonic  15996  cvgrat  16020  mertenslem1  16021  zprod  16072  fprodmodd  16132  bpolylem  16182  bpolysum  16187  bpolydiflem  16188  fsumkthpow  16190  rpnnen2lem12  16361  dvdsval3  16394  negdvdsb  16410  dvdsnegb  16411  dvdsmul1  16415  dvdsabseq  16451  dvdsssfz1  16456  odd2np1  16479  divalglem8  16538  ndvdsadd  16548  dfgcd2  16684  dvdssqim  16692  nn0seqcvgd  16708  seq1st  16709  algcvgblem  16715  lcmf  16771  lcmfunsnlem2  16778  cncongr2  16806  prmdvdsfz  16844  isprm7  16847  prmndvdsfaclt  16864  powm2modprm  16943  modprm0  16945  modprmn0modprm0  16947  pythagtriplem1  16956  pythagtriplem4  16959  pythagtriplem8  16963  pythagtriplem9  16964  pythagtriplem12  16966  pythagtriplem14  16968  pythagtriplem16  16970  pcexp  16999  pc2dvds  17019  pcz  17021  fldivp1  17037  pcfac  17039  oddprmdvds  17043  pockthg  17046  infpnlem1  17050  prmreclem1  17056  prmreclem2  17057  1arith  17067  4sqlem11  17095  vdwlem2  17122  vdwlem8  17128  vdwnnlem2  17136  prmgaplem7  17197  prmgaplem8  17198  cshwshashlem2  17236  cshwshashlem3  17237  pwsval  17619  isacs1i  17793  funcsetcestrclem9  18299  ismgmid  18807  mgmhmpropd  18849  mhmpropd  18949  smndex1gid  19062  smndex1gidOLD  19063  smndex1id  19072  grpsubid1  19197  mulgnnp1  19254  mulgsubcl  19260  mulgnn0z  19273  mulgnndir  19275  mulgneg2  19280  lagsubg  19372  ghmco  19412  symg2bas  19569  symgextfv  19594  pgpfi2  19782  efgsfo  19915  frgpupf  19949  frgpup1  19951  gsummptshft  20112  telgsumfzslem  20164  telgsums  20169  ablfac1eu  20251  pgpfac1lem2  20253  ablfaclem3  20265  dvdsrid  20559  dvdsrneg  20562  dvr1  20599  abv1  21044  lmodfopne  21137  lbsexg  21404  xrsds  21678  znf1o  21819  lindfmm  22095  lindsdom  22118  lindsenlbs  22119  gsummoncoe1  22588  matecl  22702  mavmul0g  22830  gsummatr01  22936  matunitlindflem2  22957  mp2pm2mplem4  23089  chfacfisf  23134  chfacfisfcpmat  23135  chfacfpmmulgsum2  23145  cpmadugsumlemF  23156  isclo  23367  resttopon  23441  restcld  23452  restcls  23461  iscn  23515  iscnp  23517  cnco  23546  cndis  23571  cnindis  23572  cmpsub  23680  hauscmplem  23686  cmpfii  23689  ptcnplem  23902  txtube  23921  txcmplem1  23922  xkoptsub  23935  qtoptop  23981  kqfval  24004  hmeoco  24053  fileln0  24131  trfil1  24167  trfil2  24168  trufil  24191  elfm3  24231  hausflf2  24279  isucn  24558  bl2in  24681  metss2lem  24792  metss2  24793  stdbdxmet  24796  metrest  24805  nmval2  24873  nmoix  25010  ioo2bl  25074  xrsxmet  25091  expcn  25155  elcncf  25172  icccvx  25233  cphsscph  25534  iscmet3  25576  causs  25581  metcld2  25590  metsscmetcld  25598  cncmet  25605  bcth3  25614  ovolgelb  25763  ovolfi  25777  shft2rab  25791  uniioombllem3  25868  dyadmax  25881  dyadmbl  25883  subopnmbl  25887  volcn  25889  mbfid  25918  mbfeqalem2  25925  mbfres  25927  cnmbf  25942  i1fmulc  25986  mbfi1fseqlem3  26000  mbfi1fseqlem4  26001  itg2seq  26025  itg2gt0  26043  itgss3  26097  dvexp  26235  plypow  26485  plyeq0lem  26491  coeidlem  26518  dgrlt  26547  dgrcolem2  26555  elqaalem2  26607  aacjcl  26618  aaliou3lem1  26633  aaliou3lem2  26634  pserdvlem2  26719  abelthlem8  26730  cosord  26823  sinord  26826  resinf1o  26828  relogexp  26888  logdivlt  26913  advlogexp  26947  logcxp  26961  cxpcl  26966  rpcxpcl  26968  cxpne0  26969  logbchbase  27063  logbgt0b  27085  birthdaylem2  27244  cxplim  27263  divsqrtsumo1  27275  zetacvg  27306  wilthlem1  27359  ftalem7  27370  basellem1  27372  issqf  27427  sqf11  27430  sgmf  27436  sgmnncl  27438  sqff1o  27473  dvdsflsumcom  27479  mpodvdsmulf1o  27485  dvdsmulf1o  27487  sgmppw  27488  chtublem  27502  chtub  27503  logexprlim  27516  bposlem3  27577  bposlem5  27579  bposlem6  27580  lgsdirnn0  27635  gausslemma2dlem1a  27656  gausslemma2dlem5a  27661  lgsquad2  27677  lgsquad3  27678  2sqreulem1  27737  2sqreunnlem1  27740  dchrisumlem1  27780  dchrisumlem2  27781  dchrisumlem3  27782  mulogsumlem  27822  noextenddif  27959  addsrid  28284  ltnegs  28365  lenegs  28366  om2noseqlt2  28620  elzn0s  28718  eln0zs  28720  peano5uzs  28724  bdayfinbndlem1  28787  brbtwn  29411  uspgrupgrushgr  29694  usgrumgruspgr  29697  cusgrfilem2  29971  finsumvtxdg2ssteplem2  30061  pthhashvtx  30249  cyclnumvtx  30322  crctcshwlkn0lem4  30336  crctcshwlkn0lem6  30338  crctcshwlkn0lem7  30339  crctcshwlkn0  30344  elwspths2spth  30493  rusgrnumwwlk  30501  clwlkclwwlklem2fv2  30521  erclwwlknref  30594  1to2vfriswmgr  30814  4cycl2v2nb  30824  frgr2wwlkeqm  30866  nvo00  31297  nmorepnf  31304  ubthlem1  31406  normpyc  31682  occon3  31833  pjpreeq  31934  idcnop  32517  riesz3i  32598  cnlnssadj  32616  rnbra  32643  strlem3a  32788  cvcon3  32820  ssdmd1  32849  ssdmd2  32850  relfi  33130  fcobijfs2  33248  fzsplit3  33319  prmsimpcyc  33723  esumcst  34629  dmvlsiga  34695  ballotlemimin  35073  bnj545  35460  bnj929  35501  bnj953  35504  fineqvnttrclselem1  35714  derangsn  35856  iscvm  35945  cvmsval  35952  cvmliftlem7  35977  cvmlift2lem12  36000  mclsssvlem  36248  supfz  36415  faclimlem3  36431  opnrebl2  37031  nn0prpwlem  37032  tailval  37083  nndivlub  37168  ctbssinf  38249  finixpnum  38448  ltflcei  38451  poimirlem4  38462  poimirlem14  38472  poimirlem15  38473  poimirlem19  38477  poimirlem20  38478  poimirlem22  38480  poimirlem24  38482  poimirlem28  38486  poimirlem30  38488  poimirlem31  38489  mblfinlem2  38496  mblfinlem3  38497  mblfinlem4  38498  ftc1anclem1  38531  ftc1anclem4  38534  ftc1anclem5  38535  ftc1anclem7  38537  ftc1anclem8  38538  ftc1anc  38539  caushft  38615  ismtyval  38654  heiborlem7  38671  heiborlem10  38674  heibor  38675  lcmineqlem8  43006  deg1gprod  43110  oexpreposd  43301  elrfirn  43644  ismrc  43650  nacsfix  43661  mzpcompact2lem  43700  eldiophb  43706  ellz1  43716  rexrabdioph  43739  congrep  43918  jm2.26a  43945  rngunsnply  44114  mendring  44133  iocmbl  44158  oeord2lim  44254  cantnfresb  44269  omabs2  44277  ofoafg  44299  dfno2  44372  rp-isfinite5  44461  enrelmap  44941  expgrowthi  45261  hashnnltb  45950  cnfex  45966  xlimclim2lem  46771  climxlim2  46778  icccncfext  46819  itgsinexp  46887  iblspltprt  46905  itgspltprt  46911  fourierdlem50  47088  fourierswlem  47162  etransclem35  47201  zm1nn  48294  subsubelfzo0  48319  ceilbi  48329  addmodne  48342  m1modmmod  48356  modlt0b  48361  iccpartres  48422  iccelpart  48437  iccpartiun  48438  iccpartnel  48442  nprmmul1  48531  goldbachthlem1  48552  goldbachth  48554  odz2prm2pw  48570  2pwp1prm  48596  evenltle  48737  fpprwpprb  48760  sbgoldbaltlem2  48800  bgoldbachlt  48833  isubgredg  48886  gricushgr  48937  uhgrimisgrgriclem  48950  gpgvtx0  49073  gpg5nbgrvtx13starlem2  49092  upgrwlkupwlk  49160  2zrngamgm  49264  lincresunit3  49515  lincreslvec3  49516  isldepslvec2  49519  blengt1fldiv2p1  49627  dignn0flhalf  49652  nn0sumshdiglemA  49653  rrx2pnedifcoorneor  49750  precofval2  50399  aacllem  50861