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  4396  opswapg  5214  coexg  5272  iotass  5295  resdif  5593  fvexg  5645  isotr  5939  xpexgALT  6276  ixpssmapg  6873  mapen  7003  mapdom1g  7004  elfir  7136  cauappcvgprlemladdfl  7838  addgt0sr  7958  axmulass  8056  axdistr  8057  negeu  8333  ltaddnegr  8568  nnsub  9145  zltnle  9488  ltsubnn0  9510  elz2  9514  uzaddcl  9777  qaddcl  9826  xltneg  10028  xleneg  10029  iccneg  10181  uzsubsubfz  10239  fzsplit2  10242  fzss1  10255  uzsplit  10284  fz0fzdiffz0  10322  difelfzle  10326  difelfznle  10327  fzonlt0  10361  fzouzsplit  10373  fzo0addelr  10390  eluzgtdifelfzo  10398  elfzodifsumelfzo  10402  ssfzo12  10425  qltnle  10458  modfzo0difsn  10612  nn0ennn  10650  seqfveq2g  10694  ser3mono  10704  iseqf1olemjpcl  10725  iseqf1olemqpcl  10726  seqf1oglem1  10736  seqf1oglem2  10737  seqf1og  10738  fser0const  10752  mulsubdivbinom2ap  10928  faclbnd  10958  bcval4  10969  bcpasc  10983  hashfacen  11053  seq3coll  11059  ccatval1  11127  ccatval21sw  11135  ccatrn  11139  swrd0g  11187  swrdfv2  11190  swrdspsleq  11194  addlenpfx  11218  ccatpfx  11228  swrdswrd  11232  pfxccatin12lem2  11258  pfxccat3  11261  swrdccat  11262  crim  11364  mingeb  11748  fsumshftm  11951  isumshft  11996  cvgratgt0  12039  mertenslemi1  12041  prod1dc  12092  fprod1p  12105  fprodmodd  12147  negdvdsb  12313  dvdsnegb  12314  dvdsmul1  12319  dvdsabseq  12353  dvdsssfz1  12358  odd2np1  12379  ndvdsadd  12437  dvdssqim  12540  nn0seqcvgd  12558  algcvgblem  12566  cncongr2  12621  prmind2  12637  prmdvdsfz  12656  prmndvdsfaclt  12673  dvdsfi  12756  modprm0  12772  modprmn0modprm0  12774  pythagtriplem1  12783  pythagtriplem4  12786  pythagtriplem8  12790  pythagtriplem9  12791  pythagtriplem12  12793  pythagtriplem14  12795  pythagtriplem16  12797  pcexp  12827  pc2dvds  12848  pcz  12850  fldivp1  12866  pcfac  12868  oddprmdvds  12872  pockthg  12875  infpnlem1  12877  1arith  12885  4sqlem11  12919  pwsval  13319  ismgmid  13405  mhmpropd  13494  grpsubid1  13613  mulgnnp1  13662  mulgsubcl  13668  mulgnn0z  13681  mulgnndir  13683  mulgneg2  13688  ghmco  13796  gsumfzfsumlemm  14545  resttopon  14839  cnovex  14864  iscn  14865  iscnp  14867  cnco  14889  cndis  14909  hmeoco  14984  bl2in  15071  metss2lem  15165  metss2  15166  bdxmet  15169  metrest  15174  ioo2bl  15219  expcn  15237  elcncf  15241  dvexp  15379  plypow  15412  relogexp  15540  logcxp  15565  wilthlem1  15648  sgmnncl  15656  mpodvdsmulf1o  15658  lgsdirnn0  15720  gausslemma2dlem1a  15731  lgsquadlem1  15750  lgsquad2  15756  lgsquad3  15757  uspgrupgrushgr  15974  usgrumgruspgr  15977  wksfval  16028  supfz  16398