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  8518  ltaddnegr  8754  nnsub  9345  zltnle  9694  ltsubnn0  9716  elz2  9720  uzaddcl  9995  qaddcl  10044  xltneg  10248  xleneg  10249  iccneg  10401  uzsubsubfz  10462  fzsplit2  10465  fzsplit3  10468  fzss1  10479  uzsplit  10509  fz0fzdiffz0  10547  difelfzle  10551  difelfznle  10552  fzonlt0  10586  fzouzsplit  10598  fzo0addelr  10617  eluzgtdifelfzo  10625  elfzodifsumelfzo  10629  ssfzo12  10652  infssfzcldc  10679  infssfzledc  10680  qltnle  10688  modfzo0difsn  10845  nn0ennn  10883  seqfveq2g  10927  ser3mono  10937  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  seqf1oglem1  10969  seqf1oglem2  10970  seqf1og  10971  fser0const  10985  mulsubdivbinom2ap  11163  faclbnd  11193  bcval4  11204  bcpasc  11218  hashfibclem  11296  hashfacen  11298  seq3coll  11308  ccatval1  11379  ccatval21sw  11387  ccatrn  11391  ccatalpha  11395  swrd0g  11446  swrdfv2  11449  swrdspsleq  11453  addlenpfx  11477  ccatpfx  11487  swrdswrd  11491  pfxccatin12lem2  11517  pfxccat3  11520  swrdccat  11521  crim  11637  mingeb  12024  fsumshftm  12228  isumshft  12273  cvgratgt0  12316  mertenslemi1  12318  prod1dc  12369  fprod1p  12382  fprodmodd  12424  negdvdsb  12590  dvdsnegb  12591  dvdsmul1  12596  dvdsabseq  12630  dvdsssfz1  12635  odd2np1  12656  ndvdsadd  12714  dvdssqim  12817  nn0seqcvgd  12835  algcvgblem  12843  cncongr2  12898  prmind2  12914  prmdvdsfz  12934  prmndvdsfaclt  12951  dvdsfi  13037  modprm0  13053  modprmn0modprm0  13055  pythagtriplem1  13064  pythagtriplem4  13067  pythagtriplem8  13071  pythagtriplem9  13072  pythagtriplem12  13074  pythagtriplem14  13076  pythagtriplem16  13078  pcexp  13108  pc2dvds  13129  pcz  13131  fldivp1  13147  pcfac  13149  oddprmdvds  13153  pockthg  13156  infpnlem1  13158  1arith  13166  4sqlem11  13200  ballotfilemimin  13298  ballotfilemsdom  13304  ismgmid  13746  mhmpropd  13822  grpsubid1  13939  mulgnnp1  13982  mulgsubcl  13988  mulgnn0z  14001  mulgnndir  14003  mulgneg2  14008  ghmco  14116  pwsval  14253  resttopon  15321  cnovex  15346  iscn  15347  iscnp  15349  cnco  15371  cndis  15391  hmeoco  15466  bl2in  15553  metss2lem  15647  metss2  15648  bdxmet  15651  metrest  15656  ioo2bl  15701  expcn  15719  elcncf  15723  dvexp  15861  plypow  15894  relogexp  16024  logcxp  16052  birthdaylem2  16145  wilthlem1  16151  prmdvdsfi  16159  sgmnncl  16169  mpodvdsmulf1o  16185  bposlem3  16211  bposlem5  16213  lgsdirnn0  16264  gausslemma2dlem1a  16275  lgsquadlem1  16294  lgsquad2  16300  lgsquad3  16301  uspgrupgrushgr  16521  usgrumgruspgr  16524  wksfval  16661  wlkex  16664  supfz  17219