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  4308  opswapg  5117  coexg  5175  iotass  5197  resdif  5485  fvexg  5536  isotr  5819  xpexgALT  6136  ixpssmapg  6730  mapen  6848  mapdom1g  6849  elfir  6974  cauappcvgprlemladdfl  7656  addgt0sr  7776  axmulass  7874  axdistr  7875  negeu  8150  ltaddnegr  8384  nnsub  8960  zltnle  9301  ltsubnn0  9322  elz2  9326  uzaddcl  9588  qaddcl  9637  xltneg  9838  xleneg  9839  iccneg  9991  uzsubsubfz  10049  fzsplit2  10052  fzss1  10065  uzsplit  10094  fz0fzdiffz0  10132  difelfzle  10136  difelfznle  10137  fzonlt0  10169  fzouzsplit  10181  eluzgtdifelfzo  10199  elfzodifsumelfzo  10203  ssfzo12  10226  qltnle  10248  modfzo0difsn  10397  nn0ennn  10435  ser3mono  10480  iseqf1olemjpcl  10497  iseqf1olemqpcl  10498  fser0const  10518  mulsubdivbinom2ap  10693  faclbnd  10723  bcval4  10734  bcpasc  10748  hashfacen  10818  seq3coll  10824  crim  10869  mingeb  11252  fsumshftm  11455  isumshft  11500  cvgratgt0  11543  mertenslemi1  11545  prod1dc  11596  fprod1p  11609  fprodmodd  11651  negdvdsb  11816  dvdsnegb  11817  dvdsmul1  11822  dvdsabseq  11855  dvdsssfz1  11860  odd2np1  11880  ndvdsadd  11938  dvdssqim  12027  nn0seqcvgd  12043  algcvgblem  12051  cncongr2  12106  prmind2  12122  prmdvdsfz  12141  prmndvdsfaclt  12158  phisum  12242  modprm0  12256  modprmn0modprm0  12258  pythagtriplem1  12267  pythagtriplem4  12270  pythagtriplem8  12274  pythagtriplem9  12275  pythagtriplem12  12277  pythagtriplem14  12279  pythagtriplem16  12281  pcexp  12311  pc2dvds  12331  pcz  12333  fldivp1  12348  pcfac  12350  oddprmdvds  12354  pockthg  12357  infpnlem1  12359  1arith  12367  ismgmid  12801  mhmpropd  12862  grpsubid1  12960  mulgnnp1  12996  mulgsubcl  13002  mulgnn0z  13015  mulgnndir  13017  mulgneg2  13022  resttopon  13756  cnovex  13781  iscn  13782  iscnp  13784  cnco  13806  cndis  13826  hmeoco  13901  bl2in  13988  metss2lem  14082  metss2  14083  bdxmet  14086  metrest  14091  ioo2bl  14128  elcncf  14145  dvexp  14260  relogexp  14378  logcxp  14403  lgsdirnn0  14533  supfz  14904