Theorem syl2anr 288

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 287	. 2 |- ( ( ph /\ ta ) -> th )
5	4	ancoms 266	1 |- ( ( ta /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  swopo  4228  opswapg  5025  coexg  5083  iotass  5105  resdif  5389  fvexg  5440  isotr  5717  xpexgALT  6031  ixpssmapg  6622  mapen  6740  mapdom1g  6741  elfir  6861  cauappcvgprlemladdfl  7463  addgt0sr  7583  axmulass  7681  axdistr  7682  negeu  7953  ltaddnegr  8187  nnsub  8759  zltnle  9100  elz2  9122  uzaddcl  9381  qaddcl  9427  xltneg  9619  xleneg  9620  iccneg  9772  uzsubsubfz  9827  fzsplit2  9830  fzss1  9843  uzsplit  9872  fz0fzdiffz0  9907  difelfzle  9911  difelfznle  9912  fzonlt0  9944  fzouzsplit  9956  eluzgtdifelfzo  9974  elfzodifsumelfzo  9978  ssfzo12  10001  qltnle  10023  modfzo0difsn  10168  nn0ennn  10206  ser3mono  10251  iseqf1olemjpcl  10268  iseqf1olemqpcl  10269  fser0const  10289  faclbnd  10487  bcval4  10498  bcpasc  10512  hashfacen  10579  seq3coll  10585  crim  10630  fsumshftm  11214  isumshft  11259  cvgratgt0  11302  mertenslemi1  11304  negdvdsb  11509  dvdsnegb  11510  dvdsmul1  11515  dvdsabseq  11545  dvdsssfz1  11550  odd2np1  11570  ndvdsadd  11628  dvdssqim  11712  nn0seqcvgd  11722  algcvgblem  11730  cncongr2  11785  prmind2  11801  prmdvdsfz  11819  prmndvdsfaclt  11834  resttopon  12340  cnovex  12365  iscn  12366  iscnp  12368  cnco  12390  cndis  12410  hmeoco  12485  bl2in  12572  metss2lem  12666  metss2  12667  bdxmet  12670  metrest  12675  ioo2bl  12712  elcncf  12729  dvexp  12844  supfz  13237