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  4409  opswapg  5230  coexg  5288  iotass  5311  resdif  5614  fvexg  5667  isotr  5967  xpexgALT  6304  ixpssmapg  6940  mapen  7075  mapdom1g  7076  elfir  7215  cauappcvgprlemladdfl  7918  addgt0sr  8038  axmulass  8136  axdistr  8137  negeu  8412  ltaddnegr  8647  nnsub  9224  zltnle  9569  ltsubnn0  9591  elz2  9595  uzaddcl  9864  qaddcl  9913  xltneg  10115  xleneg  10116  iccneg  10268  uzsubsubfz  10327  fzsplit2  10330  fzss1  10343  uzsplit  10372  fz0fzdiffz0  10410  difelfzle  10414  difelfznle  10415  fzonlt0  10449  fzouzsplit  10461  fzo0addelr  10480  eluzgtdifelfzo  10488  elfzodifsumelfzo  10492  ssfzo12  10515  qltnle  10549  modfzo0difsn  10703  nn0ennn  10741  seqfveq2g  10785  ser3mono  10795  iseqf1olemjpcl  10816  iseqf1olemqpcl  10817  seqf1oglem1  10827  seqf1oglem2  10828  seqf1og  10829  fser0const  10843  mulsubdivbinom2ap  11019  faclbnd  11049  bcval4  11060  bcpasc  11074  hashfacen  11146  seq3coll  11152  ccatval1  11223  ccatval21sw  11231  ccatrn  11235  ccatalpha  11239  swrd0g  11290  swrdfv2  11293  swrdspsleq  11297  addlenpfx  11321  ccatpfx  11331  swrdswrd  11335  pfxccatin12lem2  11361  pfxccat3  11364  swrdccat  11365  crim  11481  mingeb  11865  fsumshftm  12069  isumshft  12114  cvgratgt0  12157  mertenslemi1  12159  prod1dc  12210  fprod1p  12223  fprodmodd  12265  negdvdsb  12431  dvdsnegb  12432  dvdsmul1  12437  dvdsabseq  12471  dvdsssfz1  12476  odd2np1  12497  ndvdsadd  12555  dvdssqim  12658  nn0seqcvgd  12676  algcvgblem  12684  cncongr2  12739  prmind2  12755  prmdvdsfz  12774  prmndvdsfaclt  12791  dvdsfi  12874  modprm0  12890  modprmn0modprm0  12892  pythagtriplem1  12901  pythagtriplem4  12904  pythagtriplem8  12908  pythagtriplem9  12909  pythagtriplem12  12911  pythagtriplem14  12913  pythagtriplem16  12915  pcexp  12945  pc2dvds  12966  pcz  12968  fldivp1  12984  pcfac  12986  oddprmdvds  12990  pockthg  12993  infpnlem1  12995  1arith  13003  4sqlem11  13037  pwsval  13437  ismgmid  13523  mhmpropd  13612  grpsubid1  13731  mulgnnp1  13780  mulgsubcl  13786  mulgnn0z  13799  mulgnndir  13801  mulgneg2  13806  ghmco  13914  gsumfzfsumlemm  14666  resttopon  14965  cnovex  14990  iscn  14991  iscnp  14993  cnco  15015  cndis  15035  hmeoco  15110  bl2in  15197  metss2lem  15291  metss2  15292  bdxmet  15295  metrest  15300  ioo2bl  15345  expcn  15363  elcncf  15367  dvexp  15505  plypow  15538  relogexp  15666  logcxp  15691  wilthlem1  15777  sgmnncl  15785  mpodvdsmulf1o  15787  lgsdirnn0  15849  gausslemma2dlem1a  15860  lgsquadlem1  15879  lgsquad2  15885  lgsquad3  15886  uspgrupgrushgr  16106  usgrumgruspgr  16109  wksfval  16246  wlkex  16249  supfz  16787