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  4361  opswapg  5178  coexg  5236  iotass  5258  resdif  5556  fvexg  5608  isotr  5898  xpexgALT  6231  ixpssmapg  6828  mapen  6958  mapdom1g  6959  elfir  7090  cauappcvgprlemladdfl  7788  addgt0sr  7908  axmulass  8006  axdistr  8007  negeu  8283  ltaddnegr  8518  nnsub  9095  zltnle  9438  ltsubnn0  9460  elz2  9464  uzaddcl  9727  qaddcl  9776  xltneg  9978  xleneg  9979  iccneg  10131  uzsubsubfz  10189  fzsplit2  10192  fzss1  10205  uzsplit  10234  fz0fzdiffz0  10272  difelfzle  10276  difelfznle  10277  fzonlt0  10311  fzouzsplit  10323  fzo0addelr  10340  eluzgtdifelfzo  10348  elfzodifsumelfzo  10352  ssfzo12  10375  qltnle  10408  modfzo0difsn  10562  nn0ennn  10600  seqfveq2g  10644  ser3mono  10654  iseqf1olemjpcl  10675  iseqf1olemqpcl  10676  seqf1oglem1  10686  seqf1oglem2  10687  seqf1og  10688  fser0const  10702  mulsubdivbinom2ap  10878  faclbnd  10908  bcval4  10919  bcpasc  10933  hashfacen  11003  seq3coll  11009  ccatval1  11076  ccatval21sw  11084  ccatrn  11088  swrd0g  11136  swrdfv2  11139  swrdspsleq  11143  addlenpfx  11167  ccatpfx  11177  swrdswrd  11181  crim  11244  mingeb  11628  fsumshftm  11831  isumshft  11876  cvgratgt0  11919  mertenslemi1  11921  prod1dc  11972  fprod1p  11985  fprodmodd  12027  negdvdsb  12193  dvdsnegb  12194  dvdsmul1  12199  dvdsabseq  12233  dvdsssfz1  12238  odd2np1  12259  ndvdsadd  12317  dvdssqim  12420  nn0seqcvgd  12438  algcvgblem  12446  cncongr2  12501  prmind2  12517  prmdvdsfz  12536  prmndvdsfaclt  12553  dvdsfi  12636  modprm0  12652  modprmn0modprm0  12654  pythagtriplem1  12663  pythagtriplem4  12666  pythagtriplem8  12670  pythagtriplem9  12671  pythagtriplem12  12673  pythagtriplem14  12675  pythagtriplem16  12677  pcexp  12707  pc2dvds  12728  pcz  12730  fldivp1  12746  pcfac  12748  oddprmdvds  12752  pockthg  12755  infpnlem1  12757  1arith  12765  4sqlem11  12799  pwsval  13198  ismgmid  13284  mhmpropd  13373  grpsubid1  13492  mulgnnp1  13541  mulgsubcl  13547  mulgnn0z  13560  mulgnndir  13562  mulgneg2  13567  ghmco  13675  gsumfzfsumlemm  14424  resttopon  14718  cnovex  14743  iscn  14744  iscnp  14746  cnco  14768  cndis  14788  hmeoco  14863  bl2in  14950  metss2lem  15044  metss2  15045  bdxmet  15048  metrest  15053  ioo2bl  15098  expcn  15116  elcncf  15120  dvexp  15258  plypow  15291  relogexp  15419  logcxp  15444  wilthlem1  15527  sgmnncl  15535  mpodvdsmulf1o  15537  lgsdirnn0  15599  gausslemma2dlem1a  15610  lgsquadlem1  15629  lgsquad2  15635  lgsquad3  15636  supfz  16151