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  4451  opswapg  5274  coexg  5332  iotass  5355  resdif  5661  fvexg  5714  isotr  6022  xpexgALT  6366  mapsnd  6970  ixpssmapg  7010  mapen  7146  mapdom1g  7147  elfir  7307  cauappcvgprlemladdfl  8022  addgt0sr  8142  axmulass  8240  axdistr  8241  negeu  8517  ltaddnegr  8753  nnsub  9343  zltnle  9690  ltsubnn0  9712  elz2  9716  uzaddcl  9986  qaddcl  10035  xltneg  10238  xleneg  10239  iccneg  10391  uzsubsubfz  10452  fzsplit2  10455  fzsplit3  10458  fzss1  10469  uzsplit  10499  fz0fzdiffz0  10537  difelfzle  10541  difelfznle  10542  fzonlt0  10576  fzouzsplit  10588  fzo0addelr  10607  eluzgtdifelfzo  10615  elfzodifsumelfzo  10619  ssfzo12  10642  infssfzcldc  10669  infssfzledc  10670  qltnle  10678  modfzo0difsn  10832  nn0ennn  10870  seqfveq2g  10914  ser3mono  10924  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  seqf1oglem1  10956  seqf1oglem2  10957  seqf1og  10958  fser0const  10972  mulsubdivbinom2ap  11149  faclbnd  11179  bcval4  11190  bcpasc  11204  hashfibclem  11282  hashfacen  11284  seq3coll  11294  ccatval1  11365  ccatval21sw  11373  ccatrn  11377  ccatalpha  11381  swrd0g  11432  swrdfv2  11435  swrdspsleq  11439  addlenpfx  11463  ccatpfx  11473  swrdswrd  11477  pfxccatin12lem2  11503  pfxccat3  11506  swrdccat  11507  crim  11623  mingeb  12008  fsumshftm  12212  isumshft  12257  cvgratgt0  12300  mertenslemi1  12302  prod1dc  12353  fprod1p  12366  fprodmodd  12408  negdvdsb  12574  dvdsnegb  12575  dvdsmul1  12580  dvdsabseq  12614  dvdsssfz1  12619  odd2np1  12640  ndvdsadd  12698  dvdssqim  12801  nn0seqcvgd  12819  algcvgblem  12827  cncongr2  12882  prmind2  12898  prmdvdsfz  12917  prmndvdsfaclt  12934  dvdsfi  13017  modprm0  13033  modprmn0modprm0  13035  pythagtriplem1  13044  pythagtriplem4  13047  pythagtriplem8  13051  pythagtriplem9  13052  pythagtriplem12  13054  pythagtriplem14  13056  pythagtriplem16  13058  pcexp  13088  pc2dvds  13109  pcz  13111  fldivp1  13127  pcfac  13129  oddprmdvds  13133  pockthg  13136  infpnlem1  13138  1arith  13146  4sqlem11  13180  ballotfilemimin  13249  ballotfilemsdom  13255  ismgmid  13697  mhmpropd  13773  grpsubid1  13890  mulgnnp1  13933  mulgsubcl  13939  mulgnn0z  13952  mulgnndir  13954  mulgneg2  13959  ghmco  14067  pwsval  14204  resttopon  15272  cnovex  15297  iscn  15298  iscnp  15300  cnco  15322  cndis  15342  hmeoco  15417  bl2in  15504  metss2lem  15598  metss2  15599  bdxmet  15602  metrest  15607  ioo2bl  15652  expcn  15670  elcncf  15674  dvexp  15812  plypow  15845  relogexp  15973  logcxp  15999  birthdaylem2  16088  wilthlem1  16094  sgmnncl  16102  mpodvdsmulf1o  16104  lgsdirnn0  16166  gausslemma2dlem1a  16177  lgsquadlem1  16196  lgsquad2  16202  lgsquad3  16203  uspgrupgrushgr  16423  usgrumgruspgr  16426  wksfval  16563  wlkex  16566  supfz  17121