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  5607  ordintdif  6435  funco  6607  resdif  6869  fvcofneq  7112  fnprb  7227  fntpb  7228  fvf1pr  7326  isotr  7355  weisoeq  7374  brrpssg  7743  findsg  7919  coexg  7951  xpexgALT  8004  fnsuppres  8214  wfrlem10OLD  8356  oaass  8597  oeword  8626  oeworde  8629  mapsnd  8924  ixpssmapg  8966  enrefnn  9085  pw2f1olem  9114  domsdomtr  9150  xpen  9178  mapen  9179  mapdom1  9180  phplem2  9242  mapfienlem1  9442  elfir  9452  wdomen2  9614  carden2b  10004  harcard  10015  isinffi  10029  acnlem  10085  acndom  10088  alephdom  10118  fin23lem21  10376  fin23lem39  10387  isf32lem5  10394  fin1a2lem12  10448  axdc3lem2  10488  ttukeylem1  10546  pwcfsdom  10620  canthp1  10691  nqereu  10966  addpqf  10981  axmulf  11183  axmulass  11194  axdistr  11195  ltaddnegr  11475  negeu  11495  fimaxre3  12211  nnsub  12307  nn0sub  12573  ltsubnn0  12574  elz2  12628  uzaddcl  12943  qaddcl  13004  xltneg  13255  xleneg  13256  supxrbnd1  13359  infxrgelb  13373  iccneg  13508  uzsubsubfz  13582  fzsplit2  13585  fzadd2  13595  fzss1  13599  uzsplit  13632  fzdif1  13641  fz0fzdiffz0  13673  difelfzle  13677  difelfznle  13678  fvffz0  13682  preduz  13686  predfz  13689  fzonlt0  13718  fzouzsplit  13730  fzo0addelr  13754  eluzgtdifelfzo  13762  elfzodifsumelfzo  13766  ssfzo12  13794  elfznelfzob  13808  fllt  13842  flflp1  13843  uzsup  13899  negmod  13953  modifeq2int  13970  modfzo0difsn  13980  modsumfzodifsn  13981  om2uzlt2i  13988  nn0ennn  14016  suppssfz  14031  seqfveq2  14061  sermono  14071  seqf1o  14080  ser1const  14095  rpexpmord  14204  mulsubdivbinom2  14297  faclbnd  14325  bcval4  14342  bcpasc  14356  hashkf  14367  hashunx  14421  fz1isolem  14496  ishashinf  14498  seqcoll  14499  ccatval1  14611  ccatval21sw  14619  ccatrn  14623  ccatalpha  14627  swrdnd0  14691  swrd0  14692  swrdfv2  14695  swrdspsleq  14699  addlenpfx  14725  ccatpfx  14735  swrdswrd  14739  pfxccatin12lem2  14765  pfxccat3  14768  swrdccat  14769  revccat  14800  repswswrd  14818  cshwmodn  14829  cshwidxmod  14837  repswcshw  14846  2cshwid  14848  2cshwcom  14850  2cshwcshw  14860  cshwcshid  14862  cshwcsh2id  14863  s1co  14868  cshco  14871  trclub  15033  shftfval  15105  seqshft  15120  crim  15150  caubnd  15393  limsuplt  15511  isercolllem2  15698  fsumcvg  15744  fsumcvg2  15759  fsumshftm  15813  fsumo1  15844  isumshft  15871  harmonic  15891  cvgrat  15915  mertenslem1  15916  zprod  15969  fprodmodd  16029  bpolylem  16080  bpolysum  16085  bpolydiflem  16086  fsumkthpow  16088  rpnnen2lem12  16257  dvdsval3  16290  negdvdsb  16306  dvdsnegb  16307  dvdsmul1  16311  dvdsabseq  16346  dvdsssfz1  16351  odd2np1  16374  divalglem8  16433  ndvdsadd  16443  dfgcd2  16579  dvdssqim  16587  nn0seqcvgd  16603  seq1st  16604  algcvgblem  16610  lcmf  16666  lcmfunsnlem2  16673  cncongr2  16701  prmdvdsfz  16738  isprm7  16741  prmndvdsfaclt  16758  powm2modprm  16836  modprm0  16838  modprmn0modprm0  16840  pythagtriplem1  16849  pythagtriplem4  16852  pythagtriplem8  16856  pythagtriplem9  16857  pythagtriplem12  16859  pythagtriplem14  16861  pythagtriplem16  16863  pcexp  16892  pc2dvds  16912  pcz  16914  fldivp1  16930  pcfac  16932  oddprmdvds  16936  pockthg  16939  infpnlem1  16943  prmreclem1  16949  prmreclem2  16950  1arith  16960  4sqlem11  16988  vdwlem2  17015  vdwlem8  17021  vdwnnlem2  17029  prmgaplem7  17090  prmgaplem8  17091  cshwshashlem2  17130  cshwshashlem3  17131  pwsval  17532  isacs1i  17701  funcsetcestrclem9  18218  ismgmid  18690  mgmhmpropd  18723  mhmpropd  18817  smndex1gid  18928  smndex1id  18936  grpsubid1  19055  mulgnnp1  19112  mulgsubcl  19118  mulgnn0z  19131  mulgnndir  19133  mulgneg2  19138  lagsubg  19225  ghmco  19266  symg2bas  19424  symgextfv  19450  pgpfi2  19638  efgsfo  19771  frgpupf  19805  frgpup1  19807  gsummptshft  19968  telgsumfzslem  20020  telgsums  20025  ablfac1eu  20107  pgpfac1lem2  20109  ablfaclem3  20121  dvdsrid  20383  dvdsrneg  20386  dvr1  20423  abv1  20842  lmodfopne  20914  lbsexg  21183  xrsds  21444  znf1o  21587  lindfmm  21864  gsummoncoe1  22327  matecl  22446  mavmul0g  22574  gsummatr01  22680  mp2pm2mplem4  22830  chfacfisf  22875  chfacfisfcpmat  22876  chfacfpmmulgsum2  22886  cpmadugsumlemF  22897  isclo  23110  resttopon  23184  restcld  23195  restcls  23204  iscn  23258  iscnp  23260  cnco  23289  cndis  23314  cnindis  23315  cmpsub  23423  hauscmplem  23429  cmpfii  23432  ptcnplem  23644  txtube  23663  txcmplem1  23664  xkoptsub  23677  qtoptop  23723  kqfval  23746  hmeoco  23795  fileln0  23873  trfil1  23909  trfil2  23910  trufil  23933  elfm3  23973  hausflf2  24021  isucn  24302  bl2in  24425  metss2lem  24539  metss2  24540  stdbdxmet  24543  metrest  24552  nmval2  24620  nmoix  24765  ioo2bl  24828  xrsxmet  24844  expcn  24909  expcnOLD  24911  elcncf  24928  icccvx  24994  cphsscph  25298  iscmet3  25340  causs  25345  metcld2  25354  metsscmetcld  25362  cncmet  25369  bcth3  25378  ovolgelb  25528  ovolfi  25542  shft2rab  25556  uniioombllem3  25633  dyadmax  25646  dyadmbl  25648  subopnmbl  25652  volcn  25654  mbfid  25683  mbfeqalem2  25690  mbfres  25692  cnmbf  25707  i1fmulc  25752  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  itg2seq  25791  itg2gt0  25809  itgss3  25864  dvexp  26005  plypow  26258  plyeq0lem  26263  coeidlem  26290  dgrlt  26320  dgrcolem2  26328  elqaalem2  26376  aacjcl  26383  aaliou3lem1  26398  aaliou3lem2  26399  pserdvlem2  26486  abelthlem8  26497  cosord  26587  sinord  26590  resinf1o  26592  relogexp  26652  logdivlt  26677  advlogexp  26711  logcxp  26725  cxpcl  26730  rpcxpcl  26732  cxpne0  26733  logbchbase  26828  logbgt0b  26850  birthdaylem2  27009  cxplim  27029  divsqrtsumo1  27041  zetacvg  27072  wilthlem1  27125  ftalem7  27136  basellem1  27138  issqf  27193  sqf11  27196  sgmf  27202  sgmnncl  27204  sqff1o  27239  dvdsflsumcom  27245  mpodvdsmulf1o  27251  dvdsmulf1o  27253  sgmppw  27255  chtublem  27269  chtub  27270  logexprlim  27283  bposlem3  27344  bposlem5  27346  bposlem6  27347  lgsdirnn0  27402  gausslemma2dlem1a  27423  gausslemma2dlem5a  27428  lgsquad2  27444  lgsquad3  27445  2sqreulem1  27504  2sqreunnlem1  27507  dchrisumlem1  27547  dchrisumlem2  27548  dchrisumlem3  27549  mulogsumlem  27589  noextenddif  27727  addsrid  28011  sltneg  28091  sleneg  28092  om2noseqlt2  28320  elzn0s  28398  eln0zs  28400  peano5uzs  28404  brbtwn  28928  uspgrupgrushgr  29210  usgrumgruspgr  29213  cusgrfilem2  29488  finsumvtxdg2ssteplem2  29578  crctcshwlkn0lem4  29842  crctcshwlkn0lem6  29844  crctcshwlkn0lem7  29845  crctcshwlkn0  29850  elwspths2spth  29996  rusgrnumwwlk  30004  clwlkclwwlklem2fv2  30024  erclwwlknref  30097  1to2vfriswmgr  30307  4cycl2v2nb  30317  frgr2wwlkeqm  30359  nvo00  30789  nmorepnf  30796  ubthlem1  30898  normpyc  31174  occon3  31325  pjpreeq  31426  idcnop  32009  riesz3i  32090  cnlnssadj  32108  rnbra  32135  strlem3a  32280  cvcon3  32312  ssdmd1  32341  ssdmd2  32342  relfi  32621  fzsplit3  32801  prmsimpcyc  33216  esumcst  34043  dmvlsiga  34109  ballotlemimin  34486  bnj545  34887  bnj929  34928  bnj953  34931  pthhashvtx  35111  derangsn  35154  iscvm  35243  cvmsval  35250  cvmliftlem7  35275  cvmlift2lem12  35298  mclsssvlem  35546  supfz  35708  faclimlem3  35724  opnrebl2  36303  nn0prpwlem  36304  tailval  36355  nndivlub  36440  ctbssinf  37388  finixpnum  37591  ltflcei  37594  lindsdom  37600  lindsenlbs  37601  matunitlindflem2  37603  poimirlem4  37610  poimirlem14  37620  poimirlem15  37621  poimirlem19  37625  poimirlem20  37626  poimirlem22  37628  poimirlem24  37630  poimirlem28  37634  poimirlem30  37636  poimirlem31  37637  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  ftc1anclem1  37679  ftc1anclem4  37682  ftc1anclem5  37683  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  caushft  37747  ismtyval  37786  heiborlem7  37803  heiborlem10  37806  heibor  37807  lcmineqlem8  42017  deg1gprod  42121  f1o2d2  42252  oexpreposd  42335  elrfirn  42682  ismrc  42688  nacsfix  42699  mzpcompact2lem  42738  eldiophb  42744  ellz1  42754  rexrabdioph  42781  congrep  42961  jm2.26a  42988  rngunsnply  43157  mendring  43176  iocmbl  43201  oeord2lim  43298  cantnfresb  43313  omabs2  43321  ofoafg  43343  dfno2  43417  rp-isfinite5  43506  enrelmap  43986  expgrowthi  44328  cnfex  44965  xlimclim2lem  45794  climxlim2  45801  icccncfext  45842  itgsinexp  45910  iblspltprt  45928  itgspltprt  45934  fourierdlem50  46111  fourierswlem  46185  etransclem35  46224  zm1nn  47251  subsubelfzo0  47275  addmodne  47283  iccpartres  47342  iccelpart  47357  iccpartiun  47358  iccpartnel  47362  goldbachthlem1  47469  goldbachth  47471  odz2prm2pw  47487  2pwp1prm  47513  evenltle  47641  fpprwpprb  47664  sbgoldbaltlem2  47704  bgoldbachlt  47737  isubgredg  47789  gricushgr  47823  uhgrimisgrgriclem  47835  gpgvtx0  47943  gpg5nbgrvtx13starlem2  47962  upgrwlkupwlk  47983  2zrngamgm  48088  lincresunit3  48326  lincreslvec3  48327  isldepslvec2  48330  m1modmmod  48370  blengt1fldiv2p1  48442  dignn0flhalf  48467  nn0sumshdiglemA  48468  rrx2pnedifcoorneor  48565  aacllem  49031