Theorem syl2anr 290

Description: A double syllogism inference. (Contributed by NM, 17-Sep-2013.)

Hypotheses

Ref	Expression
syl2an.1	|- ( ph -> ps )
syl2an.2	|- ( ta -> ch )
syl2an.3	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
syl2anr	|- ( ( ta /\ ph ) -> th )

Proof of Theorem syl2anr

Step	Hyp	Ref	Expression
1		syl2an.1	. . 3 |- ( ph -> ps )
2		syl2an.2	. . 3 |- ( ta -> ch )
3		syl2an.3	. . 3 |- ( ( ps /\ ch ) -> th )
4	1, 2, 3	syl2an 289	. 2 |- ( ( ph /\ ta ) -> th )
5	4	ancoms 268	1 |- ( ( ta /\ ph ) -> th )

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  7151  cauappcvgprlemladdfl  7853  addgt0sr  7973  axmulass  8071  axdistr  8072  negeu  8348  ltaddnegr  8583  nnsub  9160  zltnle  9503  ltsubnn0  9525  elz2  9529  uzaddcl  9793  qaddcl  9842  xltneg  10044  xleneg  10045  iccneg  10197  uzsubsubfz  10255  fzsplit2  10258  fzss1  10271  uzsplit  10300  fz0fzdiffz0  10338  difelfzle  10342  difelfznle  10343  fzonlt0  10377  fzouzsplit  10389  fzo0addelr  10407  eluzgtdifelfzo  10415  elfzodifsumelfzo  10419  ssfzo12  10442  qltnle  10475  modfzo0difsn  10629  nn0ennn  10667  seqfveq2g  10711  ser3mono  10721  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  seqf1oglem1  10753  seqf1oglem2  10754  seqf1og  10755  fser0const  10769  mulsubdivbinom2ap  10945  faclbnd  10975  bcval4  10986  bcpasc  11000  hashfacen  11071  seq3coll  11077  ccatval1  11145  ccatval21sw  11153  ccatrn  11157  ccatalpha  11161  swrd0g  11207  swrdfv2  11210  swrdspsleq  11214  addlenpfx  11238  ccatpfx  11248  swrdswrd  11252  pfxccatin12lem2  11278  pfxccat3  11281  swrdccat  11282  crim  11384  mingeb  11768  fsumshftm  11971  isumshft  12016  cvgratgt0  12059  mertenslemi1  12061  prod1dc  12112  fprod1p  12125  fprodmodd  12167  negdvdsb  12333  dvdsnegb  12334  dvdsmul1  12339  dvdsabseq  12373  dvdsssfz1  12378  odd2np1  12399  ndvdsadd  12457  dvdssqim  12560  nn0seqcvgd  12578  algcvgblem  12586  cncongr2  12641  prmind2  12657  prmdvdsfz  12676  prmndvdsfaclt  12693  dvdsfi  12776  modprm0  12792  modprmn0modprm0  12794  pythagtriplem1  12803  pythagtriplem4  12806  pythagtriplem8  12810  pythagtriplem9  12811  pythagtriplem12  12813  pythagtriplem14  12815  pythagtriplem16  12817  pcexp  12847  pc2dvds  12868  pcz  12870  fldivp1  12886  pcfac  12888  oddprmdvds  12892  pockthg  12895  infpnlem1  12897  1arith  12905  4sqlem11  12939  pwsval  13339  ismgmid  13425  mhmpropd  13514  grpsubid1  13633  mulgnnp1  13682  mulgsubcl  13688  mulgnn0z  13701  mulgnndir  13703  mulgneg2  13708  ghmco  13816  gsumfzfsumlemm  14566  resttopon  14860  cnovex  14885  iscn  14886  iscnp  14888  cnco  14910  cndis  14930  hmeoco  15005  bl2in  15092  metss2lem  15186  metss2  15187  bdxmet  15190  metrest  15195  ioo2bl  15240  expcn  15258  elcncf  15262  dvexp  15400  plypow  15433  relogexp  15561  logcxp  15586  wilthlem1  15669  sgmnncl  15677  mpodvdsmulf1o  15679  lgsdirnn0  15741  gausslemma2dlem1a  15752  lgsquadlem1  15771  lgsquad2  15777  lgsquad3  15778  uspgrupgrushgr  15995  usgrumgruspgr  15998  wksfval  16063  wlkex  16066  supfz  16499