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  4432  opswapg  5254  coexg  5312  iotass  5335  resdif  5641  fvexg  5694  isotr  5995  xpexgALT  6339  mapsnd  6936  ixpssmapg  6976  mapen  7112  mapdom1g  7113  elfir  7273  cauappcvgprlemladdfl  7986  addgt0sr  8106  axmulass  8204  axdistr  8205  negeu  8480  ltaddnegr  8716  nnsub  9293  zltnle  9640  ltsubnn0  9662  elz2  9666  uzaddcl  9936  qaddcl  9985  xltneg  10188  xleneg  10189  iccneg  10341  uzsubsubfz  10401  fzsplit2  10404  fzsplit3  10407  fzss1  10418  uzsplit  10448  fz0fzdiffz0  10486  difelfzle  10490  difelfznle  10491  fzonlt0  10525  fzouzsplit  10537  fzo0addelr  10556  eluzgtdifelfzo  10564  elfzodifsumelfzo  10568  ssfzo12  10591  infssfzcldc  10618  infssfzledc  10619  qltnle  10627  modfzo0difsn  10781  nn0ennn  10819  seqfveq2g  10863  ser3mono  10873  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  seqf1oglem1  10905  seqf1oglem2  10906  seqf1og  10907  fser0const  10921  mulsubdivbinom2ap  11098  faclbnd  11128  bcval4  11139  bcpasc  11153  hashfibclem  11231  hashfacen  11233  seq3coll  11239  ccatval1  11310  ccatval21sw  11318  ccatrn  11322  ccatalpha  11326  swrd0g  11377  swrdfv2  11380  swrdspsleq  11384  addlenpfx  11408  ccatpfx  11418  swrdswrd  11422  pfxccatin12lem2  11448  pfxccat3  11451  swrdccat  11452  crim  11568  mingeb  11952  fsumshftm  12156  isumshft  12201  cvgratgt0  12244  mertenslemi1  12246  prod1dc  12297  fprod1p  12310  fprodmodd  12352  negdvdsb  12518  dvdsnegb  12519  dvdsmul1  12524  dvdsabseq  12558  dvdsssfz1  12563  odd2np1  12584  ndvdsadd  12642  dvdssqim  12745  nn0seqcvgd  12763  algcvgblem  12771  cncongr2  12826  prmind2  12842  prmdvdsfz  12861  prmndvdsfaclt  12878  dvdsfi  12961  modprm0  12977  modprmn0modprm0  12979  pythagtriplem1  12988  pythagtriplem4  12991  pythagtriplem8  12995  pythagtriplem9  12996  pythagtriplem12  12998  pythagtriplem14  13000  pythagtriplem16  13002  pcexp  13032  pc2dvds  13053  pcz  13055  fldivp1  13071  pcfac  13073  oddprmdvds  13077  pockthg  13080  infpnlem1  13082  1arith  13090  4sqlem11  13124  ballotfilemimin  13193  ballotfilemsdom  13199  ismgmid  13640  mhmpropd  13721  grpsubid1  13840  mulgnnp1  13883  mulgsubcl  13889  mulgnn0z  13902  mulgnndir  13904  mulgneg2  13909  ghmco  14017  pwsval  14146  gsumfzfsumlemm  14861  resttopon  15162  cnovex  15187  iscn  15188  iscnp  15190  cnco  15212  cndis  15232  hmeoco  15307  bl2in  15394  metss2lem  15488  metss2  15489  bdxmet  15492  metrest  15497  ioo2bl  15542  expcn  15560  elcncf  15564  dvexp  15702  plypow  15735  relogexp  15863  logcxp  15888  wilthlem1  15974  sgmnncl  15982  mpodvdsmulf1o  15984  lgsdirnn0  16046  gausslemma2dlem1a  16057  lgsquadlem1  16076  lgsquad2  16082  lgsquad3  16083  uspgrupgrushgr  16303  usgrumgruspgr  16306  wksfval  16443  wlkex  16446  supfz  16983