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  4374  opswapg  5191  coexg  5249  iotass  5272  resdif  5570  fvexg  5622  isotr  5913  xpexgALT  6248  ixpssmapg  6845  mapen  6975  mapdom1g  6976  elfir  7108  cauappcvgprlemladdfl  7810  addgt0sr  7930  axmulass  8028  axdistr  8029  negeu  8305  ltaddnegr  8540  nnsub  9117  zltnle  9460  ltsubnn0  9482  elz2  9486  uzaddcl  9749  qaddcl  9798  xltneg  10000  xleneg  10001  iccneg  10153  uzsubsubfz  10211  fzsplit2  10214  fzss1  10227  uzsplit  10256  fz0fzdiffz0  10294  difelfzle  10298  difelfznle  10299  fzonlt0  10333  fzouzsplit  10345  fzo0addelr  10362  eluzgtdifelfzo  10370  elfzodifsumelfzo  10374  ssfzo12  10397  qltnle  10430  modfzo0difsn  10584  nn0ennn  10622  seqfveq2g  10666  ser3mono  10676  iseqf1olemjpcl  10697  iseqf1olemqpcl  10698  seqf1oglem1  10708  seqf1oglem2  10709  seqf1og  10710  fser0const  10724  mulsubdivbinom2ap  10900  faclbnd  10930  bcval4  10941  bcpasc  10955  hashfacen  11025  seq3coll  11031  ccatval1  11098  ccatval21sw  11106  ccatrn  11110  swrd0g  11158  swrdfv2  11161  swrdspsleq  11165  addlenpfx  11189  ccatpfx  11199  swrdswrd  11203  pfxccatin12lem2  11229  pfxccat3  11232  swrdccat  11233  crim  11335  mingeb  11719  fsumshftm  11922  isumshft  11967  cvgratgt0  12010  mertenslemi1  12012  prod1dc  12063  fprod1p  12076  fprodmodd  12118  negdvdsb  12284  dvdsnegb  12285  dvdsmul1  12290  dvdsabseq  12324  dvdsssfz1  12329  odd2np1  12350  ndvdsadd  12408  dvdssqim  12511  nn0seqcvgd  12529  algcvgblem  12537  cncongr2  12592  prmind2  12608  prmdvdsfz  12627  prmndvdsfaclt  12644  dvdsfi  12727  modprm0  12743  modprmn0modprm0  12745  pythagtriplem1  12754  pythagtriplem4  12757  pythagtriplem8  12761  pythagtriplem9  12762  pythagtriplem12  12764  pythagtriplem14  12766  pythagtriplem16  12768  pcexp  12798  pc2dvds  12819  pcz  12821  fldivp1  12837  pcfac  12839  oddprmdvds  12843  pockthg  12846  infpnlem1  12848  1arith  12856  4sqlem11  12890  pwsval  13290  ismgmid  13376  mhmpropd  13465  grpsubid1  13584  mulgnnp1  13633  mulgsubcl  13639  mulgnn0z  13652  mulgnndir  13654  mulgneg2  13659  ghmco  13767  gsumfzfsumlemm  14516  resttopon  14810  cnovex  14835  iscn  14836  iscnp  14838  cnco  14860  cndis  14880  hmeoco  14955  bl2in  15042  metss2lem  15136  metss2  15137  bdxmet  15140  metrest  15145  ioo2bl  15190  expcn  15208  elcncf  15212  dvexp  15350  plypow  15383  relogexp  15511  logcxp  15536  wilthlem1  15619  sgmnncl  15627  mpodvdsmulf1o  15629  lgsdirnn0  15691  gausslemma2dlem1a  15702  lgsquadlem1  15721  lgsquad2  15727  lgsquad3  15728  uspgrupgrushgr  15945  usgrumgruspgr  15948  supfz  16350