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  5603  ordintdif  6434  funco  6606  resdif  6869  fvcofneq  7113  fnprb  7228  fntpb  7229  fvf1pr  7327  isotr  7356  weisoeq  7375  brrpssg  7745  findsg  7919  coexg  7951  resf1extb  7956  xpexgALT  8006  fnsuppres  8216  wfrlem10OLD  8358  oaass  8599  oeword  8628  oeworde  8631  mapsnd  8926  ixpssmapg  8968  enrefnn  9087  pw2f1olem  9116  domsdomtr  9152  xpen  9180  mapen  9181  mapdom1  9182  phplem2  9245  mapfienlem1  9445  elfir  9455  wdomen2  9617  carden2b  10007  harcard  10018  isinffi  10032  acnlem  10088  acndom  10091  alephdom  10121  fin23lem21  10379  fin23lem39  10390  isf32lem5  10397  fin1a2lem12  10451  axdc3lem2  10491  ttukeylem1  10549  pwcfsdom  10623  canthp1  10694  nqereu  10969  addpqf  10984  axmulf  11186  axmulass  11197  axdistr  11198  ltaddnegr  11478  negeu  11498  fimaxre3  12214  nnsub  12310  nn0sub  12576  ltsubnn0  12577  elz2  12631  uzaddcl  12946  qaddcl  13007  xltneg  13259  xleneg  13260  supxrbnd1  13363  infxrgelb  13377  iccneg  13512  uzsubsubfz  13586  fzsplit2  13589  fzadd2  13599  fzss1  13603  uzsplit  13636  fzdif1  13645  fz0fzdiffz0  13677  difelfzle  13681  difelfznle  13682  fvffz0  13686  preduz  13690  predfz  13693  fzonlt0  13722  fzouzsplit  13734  fzo0addelr  13758  eluzgtdifelfzo  13766  elfzodifsumelfzo  13770  ssfzo12  13798  elfznelfzob  13812  fllt  13846  flflp1  13847  uzsup  13903  negmod  13957  modifeq2int  13974  modfzo0difsn  13984  modsumfzodifsn  13985  om2uzlt2i  13992  nn0ennn  14020  suppssfz  14035  seqfveq2  14065  sermono  14075  seqf1o  14084  ser1const  14099  rpexpmord  14208  mulsubdivbinom2  14301  faclbnd  14329  bcval4  14346  bcpasc  14360  hashkf  14371  hashunx  14425  fz1isolem  14500  ishashinf  14502  seqcoll  14503  ccatval1  14615  ccatval21sw  14623  ccatrn  14627  ccatalpha  14631  swrdnd0  14695  swrd0  14696  swrdfv2  14699  swrdspsleq  14703  addlenpfx  14729  ccatpfx  14739  swrdswrd  14743  pfxccatin12lem2  14769  pfxccat3  14772  swrdccat  14773  revccat  14804  repswswrd  14822  cshwmodn  14833  cshwidxmod  14841  repswcshw  14850  2cshwid  14852  2cshwcom  14854  2cshwcshw  14864  cshwcshid  14866  cshwcsh2id  14867  s1co  14872  cshco  14875  trclub  15037  shftfval  15109  seqshft  15124  crim  15154  caubnd  15397  limsuplt  15515  isercolllem2  15702  fsumcvg  15748  fsumcvg2  15763  fsumshftm  15817  fsumo1  15848  isumshft  15875  harmonic  15895  cvgrat  15919  mertenslem1  15920  zprod  15973  fprodmodd  16033  bpolylem  16084  bpolysum  16089  bpolydiflem  16090  fsumkthpow  16092  rpnnen2lem12  16261  dvdsval3  16294  negdvdsb  16310  dvdsnegb  16311  dvdsmul1  16315  dvdsabseq  16350  dvdsssfz1  16355  odd2np1  16378  divalglem8  16437  ndvdsadd  16447  dfgcd2  16583  dvdssqim  16591  nn0seqcvgd  16607  seq1st  16608  algcvgblem  16614  lcmf  16670  lcmfunsnlem2  16677  cncongr2  16705  prmdvdsfz  16742  isprm7  16745  prmndvdsfaclt  16762  powm2modprm  16841  modprm0  16843  modprmn0modprm0  16845  pythagtriplem1  16854  pythagtriplem4  16857  pythagtriplem8  16861  pythagtriplem9  16862  pythagtriplem12  16864  pythagtriplem14  16866  pythagtriplem16  16868  pcexp  16897  pc2dvds  16917  pcz  16919  fldivp1  16935  pcfac  16937  oddprmdvds  16941  pockthg  16944  infpnlem1  16948  prmreclem1  16954  prmreclem2  16955  1arith  16965  4sqlem11  16993  vdwlem2  17020  vdwlem8  17026  vdwnnlem2  17034  prmgaplem7  17095  prmgaplem8  17096  cshwshashlem2  17134  cshwshashlem3  17135  pwsval  17531  isacs1i  17700  funcsetcestrclem9  18208  ismgmid  18678  mgmhmpropd  18711  mhmpropd  18805  smndex1gid  18916  smndex1id  18924  grpsubid1  19043  mulgnnp1  19100  mulgsubcl  19106  mulgnn0z  19119  mulgnndir  19121  mulgneg2  19126  lagsubg  19213  ghmco  19254  symg2bas  19410  symgextfv  19436  pgpfi2  19624  efgsfo  19757  frgpupf  19791  frgpup1  19793  gsummptshft  19954  telgsumfzslem  20006  telgsums  20011  ablfac1eu  20093  pgpfac1lem2  20095  ablfaclem3  20107  dvdsrid  20367  dvdsrneg  20370  dvr1  20407  abv1  20826  lmodfopne  20898  lbsexg  21166  xrsds  21427  znf1o  21570  lindfmm  21847  gsummoncoe1  22312  matecl  22431  mavmul0g  22559  gsummatr01  22665  mp2pm2mplem4  22815  chfacfisf  22860  chfacfisfcpmat  22861  chfacfpmmulgsum2  22871  cpmadugsumlemF  22882  isclo  23095  resttopon  23169  restcld  23180  restcls  23189  iscn  23243  iscnp  23245  cnco  23274  cndis  23299  cnindis  23300  cmpsub  23408  hauscmplem  23414  cmpfii  23417  ptcnplem  23629  txtube  23648  txcmplem1  23649  xkoptsub  23662  qtoptop  23708  kqfval  23731  hmeoco  23780  fileln0  23858  trfil1  23894  trfil2  23895  trufil  23918  elfm3  23958  hausflf2  24006  isucn  24287  bl2in  24410  metss2lem  24524  metss2  24525  stdbdxmet  24528  metrest  24537  nmval2  24605  nmoix  24750  ioo2bl  24814  xrsxmet  24831  expcn  24896  expcnOLD  24898  elcncf  24915  icccvx  24981  cphsscph  25285  iscmet3  25327  causs  25332  metcld2  25341  metsscmetcld  25349  cncmet  25356  bcth3  25365  ovolgelb  25515  ovolfi  25529  shft2rab  25543  uniioombllem3  25620  dyadmax  25633  dyadmbl  25635  subopnmbl  25639  volcn  25641  mbfid  25670  mbfeqalem2  25677  mbfres  25679  cnmbf  25694  i1fmulc  25738  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  itg2seq  25777  itg2gt0  25795  itgss3  25850  dvexp  25991  plypow  26244  plyeq0lem  26249  coeidlem  26276  dgrlt  26306  dgrcolem2  26314  elqaalem2  26362  aacjcl  26369  aaliou3lem1  26384  aaliou3lem2  26385  pserdvlem2  26472  abelthlem8  26483  cosord  26573  sinord  26576  resinf1o  26578  relogexp  26638  logdivlt  26663  advlogexp  26697  logcxp  26711  cxpcl  26716  rpcxpcl  26718  cxpne0  26719  logbchbase  26814  logbgt0b  26836  birthdaylem2  26995  cxplim  27015  divsqrtsumo1  27027  zetacvg  27058  wilthlem1  27111  ftalem7  27122  basellem1  27124  issqf  27179  sqf11  27182  sgmf  27188  sgmnncl  27190  sqff1o  27225  dvdsflsumcom  27231  mpodvdsmulf1o  27237  dvdsmulf1o  27239  sgmppw  27241  chtublem  27255  chtub  27256  logexprlim  27269  bposlem3  27330  bposlem5  27332  bposlem6  27333  lgsdirnn0  27388  gausslemma2dlem1a  27409  gausslemma2dlem5a  27414  lgsquad2  27430  lgsquad3  27431  2sqreulem1  27490  2sqreunnlem1  27493  dchrisumlem1  27533  dchrisumlem2  27534  dchrisumlem3  27535  mulogsumlem  27575  noextenddif  27713  addsrid  27997  sltneg  28077  sleneg  28078  om2noseqlt2  28306  elzn0s  28384  eln0zs  28386  peano5uzs  28390  brbtwn  28914  uspgrupgrushgr  29196  usgrumgruspgr  29199  cusgrfilem2  29474  finsumvtxdg2ssteplem2  29564  cyclnumvtx  29820  crctcshwlkn0lem4  29833  crctcshwlkn0lem6  29835  crctcshwlkn0lem7  29836  crctcshwlkn0  29841  elwspths2spth  29987  rusgrnumwwlk  29995  clwlkclwwlklem2fv2  30015  erclwwlknref  30088  1to2vfriswmgr  30298  4cycl2v2nb  30308  frgr2wwlkeqm  30350  nvo00  30780  nmorepnf  30787  ubthlem1  30889  normpyc  31165  occon3  31316  pjpreeq  31417  idcnop  32000  riesz3i  32081  cnlnssadj  32099  rnbra  32126  strlem3a  32271  cvcon3  32303  ssdmd1  32332  ssdmd2  32333  relfi  32615  fzsplit3  32795  prmsimpcyc  33234  esumcst  34064  dmvlsiga  34130  ballotlemimin  34508  bnj545  34909  bnj929  34950  bnj953  34953  pthhashvtx  35133  derangsn  35175  iscvm  35264  cvmsval  35271  cvmliftlem7  35296  cvmlift2lem12  35319  mclsssvlem  35567  supfz  35729  faclimlem3  35745  opnrebl2  36322  nn0prpwlem  36323  tailval  36374  nndivlub  36459  ctbssinf  37407  finixpnum  37612  ltflcei  37615  lindsdom  37621  lindsenlbs  37622  matunitlindflem2  37624  poimirlem4  37631  poimirlem14  37641  poimirlem15  37642  poimirlem19  37646  poimirlem20  37647  poimirlem22  37649  poimirlem24  37651  poimirlem28  37655  poimirlem30  37657  poimirlem31  37658  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  ftc1anclem1  37700  ftc1anclem4  37703  ftc1anclem5  37704  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  caushft  37768  ismtyval  37807  heiborlem7  37824  heiborlem10  37827  heibor  37828  lcmineqlem8  42037  deg1gprod  42141  f1o2d2  42274  oexpreposd  42357  elrfirn  42706  ismrc  42712  nacsfix  42723  mzpcompact2lem  42762  eldiophb  42768  ellz1  42778  rexrabdioph  42805  congrep  42985  jm2.26a  43012  rngunsnply  43181  mendring  43200  iocmbl  43225  oeord2lim  43322  cantnfresb  43337  omabs2  43345  ofoafg  43367  dfno2  43441  rp-isfinite5  43530  enrelmap  44010  expgrowthi  44352  cnfex  45033  xlimclim2lem  45854  climxlim2  45861  icccncfext  45902  itgsinexp  45970  iblspltprt  45988  itgspltprt  45994  fourierdlem50  46171  fourierswlem  46245  etransclem35  46284  zm1nn  47314  subsubelfzo0  47338  addmodne  47346  iccpartres  47405  iccelpart  47420  iccpartiun  47421  iccpartnel  47425  goldbachthlem1  47532  goldbachth  47534  odz2prm2pw  47550  2pwp1prm  47576  evenltle  47704  fpprwpprb  47727  sbgoldbaltlem2  47767  bgoldbachlt  47800  isubgredg  47852  gricushgr  47886  uhgrimisgrgriclem  47898  gpgvtx0  48008  gpg5nbgrvtx13starlem2  48028  upgrwlkupwlk  48056  2zrngamgm  48161  lincresunit3  48398  lincreslvec3  48399  isldepslvec2  48402  m1modmmod  48442  blengt1fldiv2p1  48514  dignn0flhalf  48539  nn0sumshdiglemA  48540  rrx2pnedifcoorneor  48637  precofval2  49064  aacllem  49320