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  4342  opswapg  5157  coexg  5215  iotass  5237  resdif  5529  fvexg  5580  isotr  5866  xpexgALT  6199  ixpssmapg  6796  mapen  6916  mapdom1g  6917  elfir  7048  cauappcvgprlemladdfl  7739  addgt0sr  7859  axmulass  7957  axdistr  7958  negeu  8234  ltaddnegr  8469  nnsub  9046  zltnle  9389  ltsubnn0  9410  elz2  9414  uzaddcl  9677  qaddcl  9726  xltneg  9928  xleneg  9929  iccneg  10081  uzsubsubfz  10139  fzsplit2  10142  fzss1  10155  uzsplit  10184  fz0fzdiffz0  10222  difelfzle  10226  difelfznle  10227  fzonlt0  10260  fzouzsplit  10272  eluzgtdifelfzo  10290  elfzodifsumelfzo  10294  ssfzo12  10317  qltnle  10350  modfzo0difsn  10504  nn0ennn  10542  seqfveq2g  10586  ser3mono  10596  iseqf1olemjpcl  10617  iseqf1olemqpcl  10618  seqf1oglem1  10628  seqf1oglem2  10629  seqf1og  10630  fser0const  10644  mulsubdivbinom2ap  10820  faclbnd  10850  bcval4  10861  bcpasc  10875  hashfacen  10945  seq3coll  10951  crim  11040  mingeb  11424  fsumshftm  11627  isumshft  11672  cvgratgt0  11715  mertenslemi1  11717  prod1dc  11768  fprod1p  11781  fprodmodd  11823  negdvdsb  11989  dvdsnegb  11990  dvdsmul1  11995  dvdsabseq  12029  dvdsssfz1  12034  odd2np1  12055  ndvdsadd  12113  dvdssqim  12216  nn0seqcvgd  12234  algcvgblem  12242  cncongr2  12297  prmind2  12313  prmdvdsfz  12332  prmndvdsfaclt  12349  dvdsfi  12432  modprm0  12448  modprmn0modprm0  12450  pythagtriplem1  12459  pythagtriplem4  12462  pythagtriplem8  12466  pythagtriplem9  12467  pythagtriplem12  12469  pythagtriplem14  12471  pythagtriplem16  12473  pcexp  12503  pc2dvds  12524  pcz  12526  fldivp1  12542  pcfac  12544  oddprmdvds  12548  pockthg  12551  infpnlem1  12553  1arith  12561  4sqlem11  12595  pwsval  12993  ismgmid  13079  mhmpropd  13168  grpsubid1  13287  mulgnnp1  13336  mulgsubcl  13342  mulgnn0z  13355  mulgnndir  13357  mulgneg2  13362  ghmco  13470  gsumfzfsumlemm  14219  resttopon  14491  cnovex  14516  iscn  14517  iscnp  14519  cnco  14541  cndis  14561  hmeoco  14636  bl2in  14723  metss2lem  14817  metss2  14818  bdxmet  14821  metrest  14826  ioo2bl  14871  expcn  14889  elcncf  14893  dvexp  15031  plypow  15064  relogexp  15192  logcxp  15217  wilthlem1  15300  sgmnncl  15308  mpodvdsmulf1o  15310  lgsdirnn0  15372  gausslemma2dlem1a  15383  lgsquadlem1  15402  lgsquad2  15408  lgsquad3  15409  supfz  15802