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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  swopo  4453  opswapg  5277  coexg  5335  iotass  5358  resdif  5664  fvexg  5717  isotr  6025  xpexgALT  6370  mapsnd  6976  ixpssmapg  7016  mapen  7152  mapdom1g  7153  elfir  7312  cauappcvgprlemladdfl  8028  addgt0sr  8148  axmulass  8246  axdistr  8247  negeu  8524  ltaddnegr  8760  nnsub  9352  zltnle  9699  ltsubnn0  9721  elz2  9725  uzaddcl  10001  qaddcl  10050  xltneg  10254  xleneg  10255  iccneg  10407  uzsubsubfz  10468  fzsplit2  10471  fzsplit3  10474  fzss1  10485  uzsplit  10515  fz0fzdiffz0  10553  difelfzle  10557  difelfznle  10558  fzonlt0  10592  fzouzsplit  10604  fzo0addelr  10623  eluzgtdifelfzo  10631  elfzodifsumelfzo  10635  ssfzo12  10658  infssfzcldc  10685  infssfzledc  10686  qltnle  10694  modfzo0difsn  10852  nn0ennn  10890  seqfveq2g  10934  ser3mono  10944  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  seqf1oglem1  10976  seqf1oglem2  10977  seqf1og  10978  fser0const  10992  mulsubdivbinom2ap  11170  faclbnd  11200  bcval4  11211  bcpasc  11225  hashfibclem  11303  hashfacen  11305  seq3coll  11315  ccatval1  11386  ccatval21sw  11394  ccatrn  11398  ccatalpha  11402  swrd0g  11453  swrdfv2  11456  swrdspsleq  11460  addlenpfx  11484  ccatpfx  11494  swrdswrd  11498  pfxccatin12lem2  11524  pfxccat3  11527  swrdccat  11528  crim  11644  mingeb  12032  fsumshftm  12236  isumshft  12281  cvgratgt0  12324  mertenslemi1  12326  prod1dc  12377  fprod1p  12390  fprodmodd  12432  negdvdsb  12598  dvdsnegb  12599  dvdsmul1  12604  dvdsabseq  12638  dvdsssfz1  12643  odd2np1  12664  ndvdsadd  12722  dvdssqim  12825  nn0seqcvgd  12843  algcvgblem  12851  cncongr2  12906  prmind2  12922  prmdvdsfz  12942  prmndvdsfaclt  12959  dvdsfi  13045  modprm0  13061  modprmn0modprm0  13063  pythagtriplem1  13072  pythagtriplem4  13075  pythagtriplem8  13079  pythagtriplem9  13080  pythagtriplem12  13082  pythagtriplem14  13084  pythagtriplem16  13086  pcexp  13116  pc2dvds  13137  pcz  13139  fldivp1  13155  pcfac  13157  oddprmdvds  13161  pockthg  13164  infpnlem1  13166  1arith  13174  4sqlem11  13208  ballotfilemimin  13306  ballotfilemsdom  13312  ismgmid  13755  mhmpropd  13831  grpsubid1  13948  mulgnnp1  13991  mulgsubcl  13997  mulgnn0z  14010  mulgnndir  14012  mulgneg2  14017  ghmco  14125  pwsval  14310  resttopon  15414  cnovex  15439  iscn  15440  iscnp  15442  cnco  15464  cndis  15484  hmeoco  15559  bl2in  15646  metss2lem  15740  metss2  15741  bdxmet  15744  metrest  15749  ioo2bl  15794  expcn  15812  elcncf  15816  dvexp  15954  plypow  15987  relogexp  16119  logcxp  16147  birthdaylem2  16243  wilthlem1  16249  prmdvdsfi  16260  sgmnncl  16274  mpodvdsmulf1o  16301  chtublem  16312  chtqub  16313  bposlem3  16330  bposlem5  16332  bposlem6  16333  lgsdirnn0  16388  gausslemma2dlem1a  16399  lgsquadlem1  16418  lgsquad2  16424  lgsquad3  16425  uspgrupgrushgr  16645  usgrumgruspgr  16648  wksfval  16785  wlkex  16788  supfz  17345