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  10434  eluzgtdifelfzo  10442  elfzodifsumelfzo  10446  ssfzo12  10469  qltnle  10503  modfzo0difsn  10657  nn0ennn  10695  seqfveq2g  10739  ser3mono  10749  iseqf1olemjpcl  10770  iseqf1olemqpcl  10771  seqf1oglem1  10781  seqf1oglem2  10782  seqf1og  10783  fser0const  10797  mulsubdivbinom2ap  10973  faclbnd  11003  bcval4  11014  bcpasc  11028  hashfacen  11100  seq3coll  11106  ccatval1  11174  ccatval21sw  11182  ccatrn  11186  ccatalpha  11190  swrd0g  11241  swrdfv2  11244  swrdspsleq  11248  addlenpfx  11272  ccatpfx  11282  swrdswrd  11286  pfxccatin12lem2  11312  pfxccat3  11315  swrdccat  11316  crim  11419  mingeb  11803  fsumshftm  12007  isumshft  12052  cvgratgt0  12095  mertenslemi1  12097  prod1dc  12148  fprod1p  12161  fprodmodd  12203  negdvdsb  12369  dvdsnegb  12370  dvdsmul1  12375  dvdsabseq  12409  dvdsssfz1  12414  odd2np1  12435  ndvdsadd  12493  dvdssqim  12596  nn0seqcvgd  12614  algcvgblem  12622  cncongr2  12677  prmind2  12693  prmdvdsfz  12712  prmndvdsfaclt  12729  dvdsfi  12812  modprm0  12828  modprmn0modprm0  12830  pythagtriplem1  12839  pythagtriplem4  12842  pythagtriplem8  12846  pythagtriplem9  12847  pythagtriplem12  12849  pythagtriplem14  12851  pythagtriplem16  12853  pcexp  12883  pc2dvds  12904  pcz  12906  fldivp1  12922  pcfac  12924  oddprmdvds  12928  pockthg  12931  infpnlem1  12933  1arith  12941  4sqlem11  12975  pwsval  13375  ismgmid  13461  mhmpropd  13550  grpsubid1  13669  mulgnnp1  13718  mulgsubcl  13724  mulgnn0z  13737  mulgnndir  13739  mulgneg2  13744  ghmco  13852  gsumfzfsumlemm  14603  resttopon  14897  cnovex  14922  iscn  14923  iscnp  14925  cnco  14947  cndis  14967  hmeoco  15042  bl2in  15129  metss2lem  15223  metss2  15224  bdxmet  15227  metrest  15232  ioo2bl  15277  expcn  15295  elcncf  15299  dvexp  15437  plypow  15470  relogexp  15598  logcxp  15623  wilthlem1  15706  sgmnncl  15714  mpodvdsmulf1o  15716  lgsdirnn0  15778  gausslemma2dlem1a  15789  lgsquadlem1  15808  lgsquad2  15814  lgsquad3  15815  uspgrupgrushgr  16035  usgrumgruspgr  16038  wksfval  16175  wlkex  16178  supfz  16678