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  4446  opswapg  5269  coexg  5327  iotass  5350  resdif  5656  fvexg  5709  isotr  6012  xpexgALT  6356  mapsnd  6960  ixpssmapg  7000  mapen  7136  mapdom1g  7137  elfir  7297  cauappcvgprlemladdfl  8012  addgt0sr  8132  axmulass  8230  axdistr  8231  negeu  8507  ltaddnegr  8743  nnsub  9322  zltnle  9669  ltsubnn0  9691  elz2  9695  uzaddcl  9965  qaddcl  10014  xltneg  10217  xleneg  10218  iccneg  10370  uzsubsubfz  10430  fzsplit2  10433  fzsplit3  10436  fzss1  10447  uzsplit  10477  fz0fzdiffz0  10515  difelfzle  10519  difelfznle  10520  fzonlt0  10554  fzouzsplit  10566  fzo0addelr  10585  eluzgtdifelfzo  10593  elfzodifsumelfzo  10597  ssfzo12  10620  infssfzcldc  10647  infssfzledc  10648  qltnle  10656  modfzo0difsn  10810  nn0ennn  10848  seqfveq2g  10892  ser3mono  10902  iseqf1olemjpcl  10923  iseqf1olemqpcl  10924  seqf1oglem1  10934  seqf1oglem2  10935  seqf1og  10936  fser0const  10950  mulsubdivbinom2ap  11127  faclbnd  11157  bcval4  11168  bcpasc  11182  hashfibclem  11260  hashfacen  11262  seq3coll  11272  ccatval1  11343  ccatval21sw  11351  ccatrn  11355  ccatalpha  11359  swrd0g  11410  swrdfv2  11413  swrdspsleq  11417  addlenpfx  11441  ccatpfx  11451  swrdswrd  11455  pfxccatin12lem2  11481  pfxccat3  11484  swrdccat  11485  crim  11601  mingeb  11986  fsumshftm  12190  isumshft  12235  cvgratgt0  12278  mertenslemi1  12280  prod1dc  12331  fprod1p  12344  fprodmodd  12386  negdvdsb  12552  dvdsnegb  12553  dvdsmul1  12558  dvdsabseq  12592  dvdsssfz1  12597  odd2np1  12618  ndvdsadd  12676  dvdssqim  12779  nn0seqcvgd  12797  algcvgblem  12805  cncongr2  12860  prmind2  12876  prmdvdsfz  12895  prmndvdsfaclt  12912  dvdsfi  12995  modprm0  13011  modprmn0modprm0  13013  pythagtriplem1  13022  pythagtriplem4  13025  pythagtriplem8  13029  pythagtriplem9  13030  pythagtriplem12  13032  pythagtriplem14  13034  pythagtriplem16  13036  pcexp  13066  pc2dvds  13087  pcz  13089  fldivp1  13105  pcfac  13107  oddprmdvds  13111  pockthg  13114  infpnlem1  13116  1arith  13124  4sqlem11  13158  ballotfilemimin  13227  ballotfilemsdom  13233  ismgmid  13674  mhmpropd  13750  grpsubid1  13867  mulgnnp1  13910  mulgsubcl  13916  mulgnn0z  13929  mulgnndir  13931  mulgneg2  13936  ghmco  14044  pwsval  14181  resttopon  15195  cnovex  15220  iscn  15221  iscnp  15223  cnco  15245  cndis  15265  hmeoco  15340  bl2in  15427  metss2lem  15521  metss2  15522  bdxmet  15525  metrest  15530  ioo2bl  15575  expcn  15593  elcncf  15597  dvexp  15735  plypow  15768  relogexp  15896  logcxp  15922  wilthlem1  16008  sgmnncl  16016  mpodvdsmulf1o  16018  lgsdirnn0  16080  gausslemma2dlem1a  16091  lgsquadlem1  16110  lgsquad2  16116  lgsquad3  16117  uspgrupgrushgr  16337  usgrumgruspgr  16340  wksfval  16477  wlkex  16480  supfz  17026