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  8023  addgt0sr  8143  axmulass  8241  axdistr  8242  negeu  8519  ltaddnegr  8755  nnsub  9346  zltnle  9695  ltsubnn0  9717  elz2  9721  uzaddcl  9996  qaddcl  10045  xltneg  10249  xleneg  10250  iccneg  10402  uzsubsubfz  10463  fzsplit2  10466  fzsplit3  10469  fzss1  10480  uzsplit  10510  fz0fzdiffz0  10548  difelfzle  10552  difelfznle  10553  fzonlt0  10587  fzouzsplit  10599  fzo0addelr  10618  eluzgtdifelfzo  10626  elfzodifsumelfzo  10630  ssfzo12  10653  infssfzcldc  10680  infssfzledc  10681  qltnle  10689  modfzo0difsn  10847  nn0ennn  10885  seqfveq2g  10929  ser3mono  10939  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  seqf1oglem1  10971  seqf1oglem2  10972  seqf1og  10973  fser0const  10987  mulsubdivbinom2ap  11165  faclbnd  11195  bcval4  11206  bcpasc  11220  hashfibclem  11298  hashfacen  11300  seq3coll  11310  ccatval1  11381  ccatval21sw  11389  ccatrn  11393  ccatalpha  11397  swrd0g  11448  swrdfv2  11451  swrdspsleq  11455  addlenpfx  11479  ccatpfx  11489  swrdswrd  11493  pfxccatin12lem2  11519  pfxccat3  11522  swrdccat  11523  crim  11639  mingeb  12027  fsumshftm  12231  isumshft  12276  cvgratgt0  12319  mertenslemi1  12321  prod1dc  12372  fprod1p  12385  fprodmodd  12427  negdvdsb  12593  dvdsnegb  12594  dvdsmul1  12599  dvdsabseq  12633  dvdsssfz1  12638  odd2np1  12659  ndvdsadd  12717  dvdssqim  12820  nn0seqcvgd  12838  algcvgblem  12846  cncongr2  12901  prmind2  12917  prmdvdsfz  12937  prmndvdsfaclt  12954  dvdsfi  13040  modprm0  13056  modprmn0modprm0  13058  pythagtriplem1  13067  pythagtriplem4  13070  pythagtriplem8  13074  pythagtriplem9  13075  pythagtriplem12  13077  pythagtriplem14  13079  pythagtriplem16  13081  pcexp  13111  pc2dvds  13132  pcz  13134  fldivp1  13150  pcfac  13152  oddprmdvds  13156  pockthg  13159  infpnlem1  13161  1arith  13169  4sqlem11  13203  ballotfilemimin  13301  ballotfilemsdom  13307  ismgmid  13750  mhmpropd  13826  grpsubid1  13943  mulgnnp1  13986  mulgsubcl  13992  mulgnn0z  14005  mulgnndir  14007  mulgneg2  14012  ghmco  14120  pwsval  14288  resttopon  15363  cnovex  15388  iscn  15389  iscnp  15391  cnco  15413  cndis  15433  hmeoco  15508  bl2in  15595  metss2lem  15689  metss2  15690  bdxmet  15693  metrest  15698  ioo2bl  15743  expcn  15761  elcncf  15765  dvexp  15903  plypow  15936  relogexp  16066  logcxp  16094  birthdaylem2  16187  wilthlem1  16193  prmdvdsfi  16204  sgmnncl  16218  mpodvdsmulf1o  16245  chtublem  16256  chtqub  16257  bposlem3  16274  bposlem5  16276  bposlem6  16277  lgsdirnn0  16332  gausslemma2dlem1a  16343  lgsquadlem1  16362  lgsquad2  16368  lgsquad3  16369  uspgrupgrushgr  16589  usgrumgruspgr  16592  wksfval  16729  wlkex  16732  supfz  17288