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  4403  opswapg  5223  coexg  5281  iotass  5304  resdif  5605  fvexg  5658  isotr  5957  xpexgALT  6295  ixpssmapg  6897  mapen  7032  mapdom1g  7033  elfir  7172  cauappcvgprlemladdfl  7875  addgt0sr  7995  axmulass  8093  axdistr  8094  negeu  8370  ltaddnegr  8605  nnsub  9182  zltnle  9525  ltsubnn0  9547  elz2  9551  uzaddcl  9820  qaddcl  9869  xltneg  10071  xleneg  10072  iccneg  10224  uzsubsubfz  10282  fzsplit2  10285  fzss1  10298  uzsplit  10327  fz0fzdiffz0  10365  difelfzle  10369  difelfznle  10370  fzonlt0  10404  fzouzsplit  10416  fzo0addelr  10435  eluzgtdifelfzo  10443  elfzodifsumelfzo  10447  ssfzo12  10470  qltnle  10504  modfzo0difsn  10658  nn0ennn  10696  seqfveq2g  10740  ser3mono  10750  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  seqf1oglem1  10782  seqf1oglem2  10783  seqf1og  10784  fser0const  10798  mulsubdivbinom2ap  10974  faclbnd  11004  bcval4  11015  bcpasc  11029  hashfacen  11101  seq3coll  11107  ccatval1  11178  ccatval21sw  11186  ccatrn  11190  ccatalpha  11194  swrd0g  11245  swrdfv2  11248  swrdspsleq  11252  addlenpfx  11276  ccatpfx  11286  swrdswrd  11290  pfxccatin12lem2  11316  pfxccat3  11319  swrdccat  11320  crim  11436  mingeb  11820  fsumshftm  12024  isumshft  12069  cvgratgt0  12112  mertenslemi1  12114  prod1dc  12165  fprod1p  12178  fprodmodd  12220  negdvdsb  12386  dvdsnegb  12387  dvdsmul1  12392  dvdsabseq  12426  dvdsssfz1  12431  odd2np1  12452  ndvdsadd  12510  dvdssqim  12613  nn0seqcvgd  12631  algcvgblem  12639  cncongr2  12694  prmind2  12710  prmdvdsfz  12729  prmndvdsfaclt  12746  dvdsfi  12829  modprm0  12845  modprmn0modprm0  12847  pythagtriplem1  12856  pythagtriplem4  12859  pythagtriplem8  12863  pythagtriplem9  12864  pythagtriplem12  12866  pythagtriplem14  12868  pythagtriplem16  12870  pcexp  12900  pc2dvds  12921  pcz  12923  fldivp1  12939  pcfac  12941  oddprmdvds  12945  pockthg  12948  infpnlem1  12950  1arith  12958  4sqlem11  12992  pwsval  13392  ismgmid  13478  mhmpropd  13567  grpsubid1  13686  mulgnnp1  13735  mulgsubcl  13741  mulgnn0z  13754  mulgnndir  13756  mulgneg2  13761  ghmco  13869  gsumfzfsumlemm  14620  resttopon  14914  cnovex  14939  iscn  14940  iscnp  14942  cnco  14964  cndis  14984  hmeoco  15059  bl2in  15146  metss2lem  15240  metss2  15241  bdxmet  15244  metrest  15249  ioo2bl  15294  expcn  15312  elcncf  15316  dvexp  15454  plypow  15487  relogexp  15615  logcxp  15640  wilthlem1  15723  sgmnncl  15731  mpodvdsmulf1o  15733  lgsdirnn0  15795  gausslemma2dlem1a  15806  lgsquadlem1  15825  lgsquad2  15831  lgsquad3  15832  uspgrupgrushgr  16052  usgrumgruspgr  16055  wksfval  16192  wlkex  16195  supfz  16727