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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  swopo  4453  opswapg  5277  coexg  5335  iotass  5358  resdif  5664  fvexg  5717  isotr  6025  xpexgALT  6370  mapsnd  6974  ixpssmapg  7014  mapen  7150  mapdom1g  7151  elfir  7312  cauappcvgprlemladdfl  8028  addgt0sr  8148  axmulass  8246  axdistr  8247  negeu  8524  ltaddnegr  8760  nnsub  9352  zltnle  9701  ltsubnn0  9723  elz2  9727  uzaddcl  10002  qaddcl  10051  xltneg  10255  xleneg  10256  iccneg  10408  uzsubsubfz  10469  fzsplit2  10472  fzsplit3  10475  fzss1  10486  uzsplit  10516  fz0fzdiffz0  10554  difelfzle  10558  difelfznle  10559  fzonlt0  10593  fzouzsplit  10605  fzo0addelr  10624  eluzgtdifelfzo  10632  elfzodifsumelfzo  10636  ssfzo12  10659  infssfzcldc  10686  infssfzledc  10687  qltnle  10695  modfzo0difsn  10853  nn0ennn  10891  seqfveq2g  10935  ser3mono  10945  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  seqf1oglem1  10977  seqf1oglem2  10978  seqf1og  10979  fser0const  10993  mulsubdivbinom2ap  11171  faclbnd  11201  bcval4  11212  bcpasc  11226  hashfibclem  11304  hashfacen  11306  seq3coll  11316  ccatval1  11387  ccatval21sw  11395  ccatrn  11399  ccatalpha  11403  swrd0g  11454  swrdfv2  11457  swrdspsleq  11461  addlenpfx  11485  ccatpfx  11495  swrdswrd  11499  pfxccatin12lem2  11525  pfxccat3  11528  swrdccat  11529  crim  11645  mingeb  12033  fsumshftm  12237  isumshft  12282  cvgratgt0  12325  mertenslemi1  12327  prod1dc  12378  fprod1p  12391  fprodmodd  12433  negdvdsb  12599  dvdsnegb  12600  dvdsmul1  12605  dvdsabseq  12639  dvdsssfz1  12644  odd2np1  12665  ndvdsadd  12723  dvdssqim  12826  nn0seqcvgd  12844  algcvgblem  12852  cncongr2  12907  prmind2  12923  prmdvdsfz  12943  prmndvdsfaclt  12960  dvdsfi  13046  modprm0  13062  modprmn0modprm0  13064  pythagtriplem1  13073  pythagtriplem4  13076  pythagtriplem8  13080  pythagtriplem9  13081  pythagtriplem12  13083  pythagtriplem14  13085  pythagtriplem16  13087  pcexp  13117  pc2dvds  13138  pcz  13140  fldivp1  13156  pcfac  13158  oddprmdvds  13162  pockthg  13165  infpnlem1  13167  1arith  13175  4sqlem11  13209  ballotfilemimin  13307  ballotfilemsdom  13313  ismgmid  13756  mhmpropd  13832  grpsubid1  13949  mulgnnp1  13992  mulgsubcl  13998  mulgnn0z  14011  mulgnndir  14013  mulgneg2  14018  ghmco  14126  pwsval  14311  resttopon  15397  cnovex  15422  iscn  15423  iscnp  15425  cnco  15447  cndis  15467  hmeoco  15542  bl2in  15629  metss2lem  15723  metss2  15724  bdxmet  15727  metrest  15732  ioo2bl  15777  expcn  15795  elcncf  15799  dvexp  15937  plypow  15970  relogexp  16102  logcxp  16130  birthdaylem2  16226  wilthlem1  16232  prmdvdsfi  16243  sgmnncl  16257  mpodvdsmulf1o  16284  chtublem  16295  chtqub  16296  bposlem3  16313  bposlem5  16315  bposlem6  16316  lgsdirnn0  16371  gausslemma2dlem1a  16382  lgsquadlem1  16401  lgsquad2  16407  lgsquad3  16408  uspgrupgrushgr  16628  usgrumgruspgr  16631  wksfval  16768  wlkex  16771  supfz  17328