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  5956  xpexgALT  6294  ixpssmapg  6896  mapen  7031  mapdom1g  7032  elfir  7171  cauappcvgprlemladdfl  7874  addgt0sr  7994  axmulass  8092  axdistr  8093  negeu  8369  ltaddnegr  8604  nnsub  9181  zltnle  9524  ltsubnn0  9546  elz2  9550  uzaddcl  9819  qaddcl  9868  xltneg  10070  xleneg  10071  iccneg  10223  uzsubsubfz  10281  fzsplit2  10284  fzss1  10297  uzsplit  10326  fz0fzdiffz0  10364  difelfzle  10368  difelfznle  10369  fzonlt0  10403  fzouzsplit  10415  fzo0addelr  10433  eluzgtdifelfzo  10441  elfzodifsumelfzo  10445  ssfzo12  10468  qltnle  10502  modfzo0difsn  10656  nn0ennn  10694  seqfveq2g  10738  ser3mono  10748  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  seqf1oglem1  10780  seqf1oglem2  10781  seqf1og  10782  fser0const  10796  mulsubdivbinom2ap  10972  faclbnd  11002  bcval4  11013  bcpasc  11027  hashfacen  11099  seq3coll  11105  ccatval1  11173  ccatval21sw  11181  ccatrn  11185  ccatalpha  11189  swrd0g  11240  swrdfv2  11243  swrdspsleq  11247  addlenpfx  11271  ccatpfx  11281  swrdswrd  11285  pfxccatin12lem2  11311  pfxccat3  11314  swrdccat  11315  crim  11418  mingeb  11802  fsumshftm  12005  isumshft  12050  cvgratgt0  12093  mertenslemi1  12095  prod1dc  12146  fprod1p  12159  fprodmodd  12201  negdvdsb  12367  dvdsnegb  12368  dvdsmul1  12373  dvdsabseq  12407  dvdsssfz1  12412  odd2np1  12433  ndvdsadd  12491  dvdssqim  12594  nn0seqcvgd  12612  algcvgblem  12620  cncongr2  12675  prmind2  12691  prmdvdsfz  12710  prmndvdsfaclt  12727  dvdsfi  12810  modprm0  12826  modprmn0modprm0  12828  pythagtriplem1  12837  pythagtriplem4  12840  pythagtriplem8  12844  pythagtriplem9  12845  pythagtriplem12  12847  pythagtriplem14  12849  pythagtriplem16  12851  pcexp  12881  pc2dvds  12902  pcz  12904  fldivp1  12920  pcfac  12922  oddprmdvds  12926  pockthg  12929  infpnlem1  12931  1arith  12939  4sqlem11  12973  pwsval  13373  ismgmid  13459  mhmpropd  13548  grpsubid1  13667  mulgnnp1  13716  mulgsubcl  13722  mulgnn0z  13735  mulgnndir  13737  mulgneg2  13742  ghmco  13850  gsumfzfsumlemm  14600  resttopon  14894  cnovex  14919  iscn  14920  iscnp  14922  cnco  14944  cndis  14964  hmeoco  15039  bl2in  15126  metss2lem  15220  metss2  15221  bdxmet  15224  metrest  15229  ioo2bl  15274  expcn  15292  elcncf  15296  dvexp  15434  plypow  15467  relogexp  15595  logcxp  15620  wilthlem1  15703  sgmnncl  15711  mpodvdsmulf1o  15713  lgsdirnn0  15775  gausslemma2dlem1a  15786  lgsquadlem1  15805  lgsquad2  15811  lgsquad3  15812  uspgrupgrushgr  16032  usgrumgruspgr  16035  wksfval  16172  wlkex  16175  supfz  16675