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  4397  opswapg  5215  coexg  5273  iotass  5296  resdif  5596  fvexg  5648  isotr  5946  xpexgALT  6284  ixpssmapg  6883  mapen  7015  mapdom1g  7016  elfir  7148  cauappcvgprlemladdfl  7850  addgt0sr  7970  axmulass  8068  axdistr  8069  negeu  8345  ltaddnegr  8580  nnsub  9157  zltnle  9500  ltsubnn0  9522  elz2  9526  uzaddcl  9789  qaddcl  9838  xltneg  10040  xleneg  10041  iccneg  10193  uzsubsubfz  10251  fzsplit2  10254  fzss1  10267  uzsplit  10296  fz0fzdiffz0  10334  difelfzle  10338  difelfznle  10339  fzonlt0  10373  fzouzsplit  10385  fzo0addelr  10403  eluzgtdifelfzo  10411  elfzodifsumelfzo  10415  ssfzo12  10438  qltnle  10471  modfzo0difsn  10625  nn0ennn  10663  seqfveq2g  10707  ser3mono  10717  iseqf1olemjpcl  10738  iseqf1olemqpcl  10739  seqf1oglem1  10749  seqf1oglem2  10750  seqf1og  10751  fser0const  10765  mulsubdivbinom2ap  10941  faclbnd  10971  bcval4  10982  bcpasc  10996  hashfacen  11066  seq3coll  11072  ccatval1  11140  ccatval21sw  11148  ccatrn  11152  swrd0g  11200  swrdfv2  11203  swrdspsleq  11207  addlenpfx  11231  ccatpfx  11241  swrdswrd  11245  pfxccatin12lem2  11271  pfxccat3  11274  swrdccat  11275  crim  11377  mingeb  11761  fsumshftm  11964  isumshft  12009  cvgratgt0  12052  mertenslemi1  12054  prod1dc  12105  fprod1p  12118  fprodmodd  12160  negdvdsb  12326  dvdsnegb  12327  dvdsmul1  12332  dvdsabseq  12366  dvdsssfz1  12371  odd2np1  12392  ndvdsadd  12450  dvdssqim  12553  nn0seqcvgd  12571  algcvgblem  12579  cncongr2  12634  prmind2  12650  prmdvdsfz  12669  prmndvdsfaclt  12686  dvdsfi  12769  modprm0  12785  modprmn0modprm0  12787  pythagtriplem1  12796  pythagtriplem4  12799  pythagtriplem8  12803  pythagtriplem9  12804  pythagtriplem12  12806  pythagtriplem14  12808  pythagtriplem16  12810  pcexp  12840  pc2dvds  12861  pcz  12863  fldivp1  12879  pcfac  12881  oddprmdvds  12885  pockthg  12888  infpnlem1  12890  1arith  12898  4sqlem11  12932  pwsval  13332  ismgmid  13418  mhmpropd  13507  grpsubid1  13626  mulgnnp1  13675  mulgsubcl  13681  mulgnn0z  13694  mulgnndir  13696  mulgneg2  13701  ghmco  13809  gsumfzfsumlemm  14559  resttopon  14853  cnovex  14878  iscn  14879  iscnp  14881  cnco  14903  cndis  14923  hmeoco  14998  bl2in  15085  metss2lem  15179  metss2  15180  bdxmet  15183  metrest  15188  ioo2bl  15233  expcn  15251  elcncf  15255  dvexp  15393  plypow  15426  relogexp  15554  logcxp  15579  wilthlem1  15662  sgmnncl  15670  mpodvdsmulf1o  15672  lgsdirnn0  15734  gausslemma2dlem1a  15745  lgsquadlem1  15764  lgsquad2  15770  lgsquad3  15771  uspgrupgrushgr  15988  usgrumgruspgr  15991  wksfval  16043  wlkex  16046  supfz  16469