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  4351  opswapg  5166  coexg  5224  iotass  5246  resdif  5538  fvexg  5589  isotr  5875  xpexgALT  6208  ixpssmapg  6805  mapen  6925  mapdom1g  6926  elfir  7057  cauappcvgprlemladdfl  7750  addgt0sr  7870  axmulass  7968  axdistr  7969  negeu  8245  ltaddnegr  8480  nnsub  9057  zltnle  9400  ltsubnn0  9422  elz2  9426  uzaddcl  9689  qaddcl  9738  xltneg  9940  xleneg  9941  iccneg  10093  uzsubsubfz  10151  fzsplit2  10154  fzss1  10167  uzsplit  10196  fz0fzdiffz0  10234  difelfzle  10238  difelfznle  10239  fzonlt0  10272  fzouzsplit  10284  fzo0addelr  10299  eluzgtdifelfzo  10307  elfzodifsumelfzo  10311  ssfzo12  10334  qltnle  10367  modfzo0difsn  10521  nn0ennn  10559  seqfveq2g  10603  ser3mono  10613  iseqf1olemjpcl  10634  iseqf1olemqpcl  10635  seqf1oglem1  10645  seqf1oglem2  10646  seqf1og  10647  fser0const  10661  mulsubdivbinom2ap  10837  faclbnd  10867  bcval4  10878  bcpasc  10892  hashfacen  10962  seq3coll  10968  ccatval1  11028  ccatval21sw  11036  ccatrn  11040  crim  11088  mingeb  11472  fsumshftm  11675  isumshft  11720  cvgratgt0  11763  mertenslemi1  11765  prod1dc  11816  fprod1p  11829  fprodmodd  11871  negdvdsb  12037  dvdsnegb  12038  dvdsmul1  12043  dvdsabseq  12077  dvdsssfz1  12082  odd2np1  12103  ndvdsadd  12161  dvdssqim  12264  nn0seqcvgd  12282  algcvgblem  12290  cncongr2  12345  prmind2  12361  prmdvdsfz  12380  prmndvdsfaclt  12397  dvdsfi  12480  modprm0  12496  modprmn0modprm0  12498  pythagtriplem1  12507  pythagtriplem4  12510  pythagtriplem8  12514  pythagtriplem9  12515  pythagtriplem12  12517  pythagtriplem14  12519  pythagtriplem16  12521  pcexp  12551  pc2dvds  12572  pcz  12574  fldivp1  12590  pcfac  12592  oddprmdvds  12596  pockthg  12599  infpnlem1  12601  1arith  12609  4sqlem11  12643  pwsval  13041  ismgmid  13127  mhmpropd  13216  grpsubid1  13335  mulgnnp1  13384  mulgsubcl  13390  mulgnn0z  13403  mulgnndir  13405  mulgneg2  13410  ghmco  13518  gsumfzfsumlemm  14267  resttopon  14561  cnovex  14586  iscn  14587  iscnp  14589  cnco  14611  cndis  14631  hmeoco  14706  bl2in  14793  metss2lem  14887  metss2  14888  bdxmet  14891  metrest  14896  ioo2bl  14941  expcn  14959  elcncf  14963  dvexp  15101  plypow  15134  relogexp  15262  logcxp  15287  wilthlem1  15370  sgmnncl  15378  mpodvdsmulf1o  15380  lgsdirnn0  15442  gausslemma2dlem1a  15453  lgsquadlem1  15472  lgsquad2  15478  lgsquad3  15479  supfz  15874