Theorem syl2anr 290

Description: A double syllogism inference. (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 289	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
5	4	ancoms 268	1 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  swopo  4429  opswapg  5251  coexg  5309  iotass  5332  resdif  5638  fvexg  5691  isotr  5991  xpexgALT  6328  mapsnd  6925  ixpssmapg  6965  mapen  7101  mapdom1g  7102  elfir  7262  cauappcvgprlemladdfl  7975  addgt0sr  8095  axmulass  8193  axdistr  8194  negeu  8469  ltaddnegr  8704  nnsub  9281  zltnle  9628  ltsubnn0  9650  elz2  9654  uzaddcl  9924  qaddcl  9973  xltneg  10175  xleneg  10176  iccneg  10328  uzsubsubfz  10387  fzsplit2  10390  fzss1  10403  uzsplit  10433  fz0fzdiffz0  10471  difelfzle  10475  difelfznle  10476  fzonlt0  10510  fzouzsplit  10522  fzo0addelr  10541  eluzgtdifelfzo  10549  elfzodifsumelfzo  10553  ssfzo12  10576  qltnle  10610  modfzo0difsn  10764  nn0ennn  10802  seqfveq2g  10846  ser3mono  10856  iseqf1olemjpcl  10877  iseqf1olemqpcl  10878  seqf1oglem1  10888  seqf1oglem2  10889  seqf1og  10890  fser0const  10904  mulsubdivbinom2ap  11081  faclbnd  11111  bcval4  11122  bcpasc  11136  hashfibclem  11214  hashfacen  11216  seq3coll  11222  ccatval1  11293  ccatval21sw  11301  ccatrn  11305  ccatalpha  11309  swrd0g  11360  swrdfv2  11363  swrdspsleq  11367  addlenpfx  11391  ccatpfx  11401  swrdswrd  11405  pfxccatin12lem2  11431  pfxccat3  11434  swrdccat  11435  crim  11551  mingeb  11935  fsumshftm  12139  isumshft  12184  cvgratgt0  12227  mertenslemi1  12229  prod1dc  12280  fprod1p  12293  fprodmodd  12335  negdvdsb  12501  dvdsnegb  12502  dvdsmul1  12507  dvdsabseq  12541  dvdsssfz1  12546  odd2np1  12567  ndvdsadd  12625  dvdssqim  12728  nn0seqcvgd  12746  algcvgblem  12754  cncongr2  12809  prmind2  12825  prmdvdsfz  12844  prmndvdsfaclt  12861  dvdsfi  12944  modprm0  12960  modprmn0modprm0  12962  pythagtriplem1  12971  pythagtriplem4  12974  pythagtriplem8  12978  pythagtriplem9  12979  pythagtriplem12  12981  pythagtriplem14  12983  pythagtriplem16  12985  pcexp  13015  pc2dvds  13036  pcz  13038  fldivp1  13054  pcfac  13056  oddprmdvds  13060  pockthg  13063  infpnlem1  13065  1arith  13073  4sqlem11  13107  pwsval  13525  ismgmid  13611  mhmpropd  13700  grpsubid1  13819  mulgnnp1  13868  mulgsubcl  13874  mulgnn0z  13887  mulgnndir  13889  mulgneg2  13894  ghmco  14002  gsumfzfsumlemm  14784  resttopon  15085  cnovex  15110  iscn  15111  iscnp  15113  cnco  15135  cndis  15155  hmeoco  15230  bl2in  15317  metss2lem  15411  metss2  15412  bdxmet  15415  metrest  15420  ioo2bl  15465  expcn  15483  elcncf  15487  dvexp  15625  plypow  15658  relogexp  15786  logcxp  15811  wilthlem1  15897  sgmnncl  15905  mpodvdsmulf1o  15907  lgsdirnn0  15969  gausslemma2dlem1a  15980  lgsquadlem1  15999  lgsquad2  16005  lgsquad3  16006  uspgrupgrushgr  16226  usgrumgruspgr  16229  wksfval  16366  wlkex  16369  supfz  16906