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  4283  opswapg  5089  coexg  5147  iotass  5169  resdif  5453  fvexg  5504  isotr  5783  xpexgALT  6098  ixpssmapg  6690  mapen  6808  mapdom1g  6809  elfir  6934  cauappcvgprlemladdfl  7592  addgt0sr  7712  axmulass  7810  axdistr  7811  negeu  8085  ltaddnegr  8319  nnsub  8892  zltnle  9233  ltsubnn0  9254  elz2  9258  uzaddcl  9520  qaddcl  9569  xltneg  9768  xleneg  9769  iccneg  9921  uzsubsubfz  9978  fzsplit2  9981  fzss1  9994  uzsplit  10023  fz0fzdiffz0  10061  difelfzle  10065  difelfznle  10066  fzonlt0  10098  fzouzsplit  10110  eluzgtdifelfzo  10128  elfzodifsumelfzo  10132  ssfzo12  10155  qltnle  10177  modfzo0difsn  10326  nn0ennn  10364  ser3mono  10409  iseqf1olemjpcl  10426  iseqf1olemqpcl  10427  fser0const  10447  faclbnd  10650  bcval4  10661  bcpasc  10675  hashfacen  10745  seq3coll  10751  crim  10796  mingeb  11179  fsumshftm  11382  isumshft  11427  cvgratgt0  11470  mertenslemi1  11472  prod1dc  11523  fprod1p  11536  fprodmodd  11578  negdvdsb  11743  dvdsnegb  11744  dvdsmul1  11749  dvdsabseq  11781  dvdsssfz1  11786  odd2np1  11806  ndvdsadd  11864  dvdssqim  11953  nn0seqcvgd  11969  algcvgblem  11977  cncongr2  12032  prmind2  12048  prmdvdsfz  12067  prmndvdsfaclt  12084  phisum  12168  modprm0  12182  modprmn0modprm0  12184  pythagtriplem1  12193  pythagtriplem4  12196  pythagtriplem8  12200  pythagtriplem9  12201  pythagtriplem12  12203  pythagtriplem14  12205  pythagtriplem16  12207  pcexp  12237  pc2dvds  12257  pcz  12259  fldivp1  12274  pcfac  12276  oddprmdvds  12280  pockthg  12283  infpnlem1  12285  1arith  12293  resttopon  12771  cnovex  12796  iscn  12797  iscnp  12799  cnco  12821  cndis  12841  hmeoco  12916  bl2in  13003  metss2lem  13097  metss2  13098  bdxmet  13101  metrest  13106  ioo2bl  13143  elcncf  13160  dvexp  13275  relogexp  13393  logcxp  13418  lgsdirnn0  13548  supfz  13907