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  4352  opswapg  5168  coexg  5226  iotass  5248  resdif  5543  fvexg  5594  isotr  5884  xpexgALT  6217  ixpssmapg  6814  mapen  6942  mapdom1g  6943  elfir  7074  cauappcvgprlemladdfl  7767  addgt0sr  7887  axmulass  7985  axdistr  7986  negeu  8262  ltaddnegr  8497  nnsub  9074  zltnle  9417  ltsubnn0  9439  elz2  9443  uzaddcl  9706  qaddcl  9755  xltneg  9957  xleneg  9958  iccneg  10110  uzsubsubfz  10168  fzsplit2  10171  fzss1  10184  uzsplit  10213  fz0fzdiffz0  10251  difelfzle  10255  difelfznle  10256  fzonlt0  10289  fzouzsplit  10301  fzo0addelr  10316  eluzgtdifelfzo  10324  elfzodifsumelfzo  10328  ssfzo12  10351  qltnle  10384  modfzo0difsn  10538  nn0ennn  10576  seqfveq2g  10620  ser3mono  10630  iseqf1olemjpcl  10651  iseqf1olemqpcl  10652  seqf1oglem1  10662  seqf1oglem2  10663  seqf1og  10664  fser0const  10678  mulsubdivbinom2ap  10854  faclbnd  10884  bcval4  10895  bcpasc  10909  hashfacen  10979  seq3coll  10985  ccatval1  11051  ccatval21sw  11059  ccatrn  11063  crim  11111  mingeb  11495  fsumshftm  11698  isumshft  11743  cvgratgt0  11786  mertenslemi1  11788  prod1dc  11839  fprod1p  11852  fprodmodd  11894  negdvdsb  12060  dvdsnegb  12061  dvdsmul1  12066  dvdsabseq  12100  dvdsssfz1  12105  odd2np1  12126  ndvdsadd  12184  dvdssqim  12287  nn0seqcvgd  12305  algcvgblem  12313  cncongr2  12368  prmind2  12384  prmdvdsfz  12403  prmndvdsfaclt  12420  dvdsfi  12503  modprm0  12519  modprmn0modprm0  12521  pythagtriplem1  12530  pythagtriplem4  12533  pythagtriplem8  12537  pythagtriplem9  12538  pythagtriplem12  12540  pythagtriplem14  12542  pythagtriplem16  12544  pcexp  12574  pc2dvds  12595  pcz  12597  fldivp1  12613  pcfac  12615  oddprmdvds  12619  pockthg  12622  infpnlem1  12624  1arith  12632  4sqlem11  12666  pwsval  13065  ismgmid  13151  mhmpropd  13240  grpsubid1  13359  mulgnnp1  13408  mulgsubcl  13414  mulgnn0z  13427  mulgnndir  13429  mulgneg2  13434  ghmco  13542  gsumfzfsumlemm  14291  resttopon  14585  cnovex  14610  iscn  14611  iscnp  14613  cnco  14635  cndis  14655  hmeoco  14730  bl2in  14817  metss2lem  14911  metss2  14912  bdxmet  14915  metrest  14920  ioo2bl  14965  expcn  14983  elcncf  14987  dvexp  15125  plypow  15158  relogexp  15286  logcxp  15311  wilthlem1  15394  sgmnncl  15402  mpodvdsmulf1o  15404  lgsdirnn0  15466  gausslemma2dlem1a  15477  lgsquadlem1  15496  lgsquad2  15502  lgsquad3  15503  supfz  15943