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  4401  opswapg  5221  coexg  5279  iotass  5302  resdif  5602  fvexg  5654  isotr  5952  xpexgALT  6290  ixpssmapg  6892  mapen  7027  mapdom1g  7028  elfir  7163  cauappcvgprlemladdfl  7865  addgt0sr  7985  axmulass  8083  axdistr  8084  negeu  8360  ltaddnegr  8595  nnsub  9172  zltnle  9515  ltsubnn0  9537  elz2  9541  uzaddcl  9810  qaddcl  9859  xltneg  10061  xleneg  10062  iccneg  10214  uzsubsubfz  10272  fzsplit2  10275  fzss1  10288  uzsplit  10317  fz0fzdiffz0  10355  difelfzle  10359  difelfznle  10360  fzonlt0  10394  fzouzsplit  10406  fzo0addelr  10424  eluzgtdifelfzo  10432  elfzodifsumelfzo  10436  ssfzo12  10459  qltnle  10493  modfzo0difsn  10647  nn0ennn  10685  seqfveq2g  10729  ser3mono  10739  iseqf1olemjpcl  10760  iseqf1olemqpcl  10761  seqf1oglem1  10771  seqf1oglem2  10772  seqf1og  10773  fser0const  10787  mulsubdivbinom2ap  10963  faclbnd  10993  bcval4  11004  bcpasc  11018  hashfacen  11090  seq3coll  11096  ccatval1  11164  ccatval21sw  11172  ccatrn  11176  ccatalpha  11180  swrd0g  11231  swrdfv2  11234  swrdspsleq  11238  addlenpfx  11262  ccatpfx  11272  swrdswrd  11276  pfxccatin12lem2  11302  pfxccat3  11305  swrdccat  11306  crim  11409  mingeb  11793  fsumshftm  11996  isumshft  12041  cvgratgt0  12084  mertenslemi1  12086  prod1dc  12137  fprod1p  12150  fprodmodd  12192  negdvdsb  12358  dvdsnegb  12359  dvdsmul1  12364  dvdsabseq  12398  dvdsssfz1  12403  odd2np1  12424  ndvdsadd  12482  dvdssqim  12585  nn0seqcvgd  12603  algcvgblem  12611  cncongr2  12666  prmind2  12682  prmdvdsfz  12701  prmndvdsfaclt  12718  dvdsfi  12801  modprm0  12817  modprmn0modprm0  12819  pythagtriplem1  12828  pythagtriplem4  12831  pythagtriplem8  12835  pythagtriplem9  12836  pythagtriplem12  12838  pythagtriplem14  12840  pythagtriplem16  12842  pcexp  12872  pc2dvds  12893  pcz  12895  fldivp1  12911  pcfac  12913  oddprmdvds  12917  pockthg  12920  infpnlem1  12922  1arith  12930  4sqlem11  12964  pwsval  13364  ismgmid  13450  mhmpropd  13539  grpsubid1  13658  mulgnnp1  13707  mulgsubcl  13713  mulgnn0z  13726  mulgnndir  13728  mulgneg2  13733  ghmco  13841  gsumfzfsumlemm  14591  resttopon  14885  cnovex  14910  iscn  14911  iscnp  14913  cnco  14935  cndis  14955  hmeoco  15030  bl2in  15117  metss2lem  15211  metss2  15212  bdxmet  15215  metrest  15220  ioo2bl  15265  expcn  15283  elcncf  15287  dvexp  15425  plypow  15458  relogexp  15586  logcxp  15611  wilthlem1  15694  sgmnncl  15702  mpodvdsmulf1o  15704  lgsdirnn0  15766  gausslemma2dlem1a  15777  lgsquadlem1  15796  lgsquad2  15802  lgsquad3  15803  uspgrupgrushgr  16021  usgrumgruspgr  16024  wksfval  16119  wlkex  16122  supfz  16611