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  4427  opswapg  5249  coexg  5307  iotass  5330  resdif  5636  fvexg  5689  isotr  5989  xpexgALT  6326  mapsnd  6923  ixpssmapg  6963  mapen  7099  mapdom1g  7100  elfir  7260  cauappcvgprlemladdfl  7970  addgt0sr  8090  axmulass  8188  axdistr  8189  negeu  8464  ltaddnegr  8699  nnsub  9276  zltnle  9623  ltsubnn0  9645  elz2  9649  uzaddcl  9918  qaddcl  9967  xltneg  10169  xleneg  10170  iccneg  10322  uzsubsubfz  10381  fzsplit2  10384  fzss1  10397  uzsplit  10426  fz0fzdiffz0  10464  difelfzle  10468  difelfznle  10469  fzonlt0  10503  fzouzsplit  10515  fzo0addelr  10534  eluzgtdifelfzo  10542  elfzodifsumelfzo  10546  ssfzo12  10569  qltnle  10603  modfzo0difsn  10757  nn0ennn  10795  seqfveq2g  10839  ser3mono  10849  iseqf1olemjpcl  10870  iseqf1olemqpcl  10871  seqf1oglem1  10881  seqf1oglem2  10882  seqf1og  10883  fser0const  10897  mulsubdivbinom2ap  11073  faclbnd  11103  bcval4  11114  bcpasc  11128  hashfibclem  11206  hashfacen  11208  seq3coll  11214  ccatval1  11285  ccatval21sw  11293  ccatrn  11297  ccatalpha  11301  swrd0g  11352  swrdfv2  11355  swrdspsleq  11359  addlenpfx  11383  ccatpfx  11393  swrdswrd  11397  pfxccatin12lem2  11423  pfxccat3  11426  swrdccat  11427  crim  11543  mingeb  11927  fsumshftm  12131  isumshft  12176  cvgratgt0  12219  mertenslemi1  12221  prod1dc  12272  fprod1p  12285  fprodmodd  12327  negdvdsb  12493  dvdsnegb  12494  dvdsmul1  12499  dvdsabseq  12533  dvdsssfz1  12538  odd2np1  12559  ndvdsadd  12617  dvdssqim  12720  nn0seqcvgd  12738  algcvgblem  12746  cncongr2  12801  prmind2  12817  prmdvdsfz  12836  prmndvdsfaclt  12853  dvdsfi  12936  modprm0  12952  modprmn0modprm0  12954  pythagtriplem1  12963  pythagtriplem4  12966  pythagtriplem8  12970  pythagtriplem9  12971  pythagtriplem12  12973  pythagtriplem14  12975  pythagtriplem16  12977  pcexp  13007  pc2dvds  13028  pcz  13030  fldivp1  13046  pcfac  13048  oddprmdvds  13052  pockthg  13055  infpnlem1  13057  1arith  13065  4sqlem11  13099  pwsval  13504  ismgmid  13590  mhmpropd  13679  grpsubid1  13798  mulgnnp1  13847  mulgsubcl  13853  mulgnn0z  13866  mulgnndir  13868  mulgneg2  13873  ghmco  13981  gsumfzfsumlemm  14735  resttopon  15036  cnovex  15061  iscn  15062  iscnp  15064  cnco  15086  cndis  15106  hmeoco  15181  bl2in  15268  metss2lem  15362  metss2  15363  bdxmet  15366  metrest  15371  ioo2bl  15416  expcn  15434  elcncf  15438  dvexp  15576  plypow  15609  relogexp  15737  logcxp  15762  wilthlem1  15848  sgmnncl  15856  mpodvdsmulf1o  15858  lgsdirnn0  15920  gausslemma2dlem1a  15931  lgsquadlem1  15950  lgsquad2  15956  lgsquad3  15957  uspgrupgrushgr  16177  usgrumgruspgr  16180  wksfval  16317  wlkex  16320  supfz  16857