Theorem sylan9eq 2483

Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
sylan9eq.1	|- ( ph -> A = B )
sylan9eq.2	|- ( ps -> B = C )

Assertion

Ref	Expression
sylan9eq	|- ( ( ph /\ ps ) -> A = C )

Proof of Theorem sylan9eq

Step	Hyp	Ref	Expression
1		sylan9eq.1	. 2 |- ( ph -> A = B )
2		sylan9eq.2	. 2 |- ( ps -> B = C )
3		eqtr 2448	. 2 |- ( ( A = B /\ B = C ) -> A = C )
4	1, 2, 3	syl2an 479	1 |- ( ( ph /\ ps ) -> A = C )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2414

This theorem is referenced by:  sylan9req  2484  sylan9eqr  2485  difeq12  3578  uneq12  3615  ineq12  3659  ifeq12  3928  ifbi  3932  preq12  4081  prprc  4112  preq12b  4176  opeq12  4189  opthwiener  4722  xpeq12  4872  sosn  4923  nfimad  5196  coi2  5371  ordintdif  5491  funimass1  5674  f1orescnv  5846  resdif  5851  fvmpt2  5973  fvmptnf  5983  oveq12  6314  cbvmpt2v  6385  ovmpt2g  6445  caofinvl  6572  eqopi  6841  fmpt2co  6890  mpt2sn  6898  supp0cosupp0  6965  mpt2curryd  7027  fvmpt2curryd  7029  wrecseq123  7040  rdgsucmptf  7157  frsucmpt  7166  oevn0  7228  oa0r  7251  om1r  7255  oe1m  7257  omass  7292  oeoalem  7308  oeoa  7309  oeoe  7311  map0g  7522  xpcomco  7671  sbthlem4  7694  sbthlem5  7695  xpmapenlem  7748  phplem3  7762  phplem4  7763  unxpdomlem3  7787  funsnfsupp  7916  ordtypelem7  8048  cardennn  8425  dfac9  8573  cdaassen  8619  alephsing  8713  axcc3  8875  ac6num  8916  konigthlem  9000  canthp1lem2  9085  ordpipq  9374  ltrnq  9411  addclprlem2  9449  mulclprlem  9451  prlem934  9465  prlem936  9479  mulcmpblnrlem  9501  addcnsr  9566  mulcnsr  9567  axcnre  9595  recex  10251  rpnnen1lem3  11299  rpnnen1lem5  11301  xaddpnf1  11526  xaddpnf2  11527  xaddmnf1  11528  xaddmnf2  11529  rexadd  11532  xaddnemnf  11534  xaddnepnf  11535  xadddilem  11587  om2uzrani  12172  om2uzrdg  12176  seqf1olem2  12259  seqf1o  12260  modexp  12413  faclbnd4lem3  12486  hashunsng  12577  lsw1  12718  swrdfv  12782  swrdccat  12851  ccats1swrdeqbi  12856  revfv  12870  cshwsublen  12900  wrdlen2  13023  wwlktovf1  13032  relexp0  13086  relexpcnv  13098  shftcan1  13146  remul2  13193  immul2  13200  sumss  13789  geomulcvg  13931  fprodss  14001  binomfallfaclem2  14092  bpolylem  14100  ef0lem  14132  efieq1re  14252  rpnnen2lem1  14266  ruclem3  14284  dvdsnegb  14319  dvdscmul  14328  dvds2ln  14332  dvds2add  14333  dvds2sub  14334  gcdn0val  14471  rpmulgcd  14522  lcmn0val  14558  lcmn0valOLD  14559  odzval  14735  odzvalOLD  14741  pcval  14793  pcmpt  14836  prmreclem4  14862  1arithlem2  14867  vdwlem8  14937  ramcl2lem  14961  ramcl2lemOLD  14962  ramtcl  14963  ramtclOLD  14964  ramtub  14967  ramtubOLD  14968  ramcl2  14972  ramcl2OLD  14973  ramcl  14986  setsval  15145  prfcl  16087  curf1cl  16112  curfcl  16116  hofcl  16143  yonedalem4c  16161  psssdm  16461  grplactval  16752  cntzval  16974  f1omvdco2  17088  pmtrfinv  17101  psgnunilem5  17134  odlem2  17187  odlem2OLD  17203  gexlem2  17232  gexlem2OLD  17235  lsmvalx  17290  efgtval  17372  efgredlema  17389  vrgpval  17416  cyggex  17531  gsumcom2  17606  dvdsrtr  17879  abvtrivd  18067  lmhmco  18265  reslmhm  18274  lvecinv  18335  mplmon2  18715  subrgasclcl  18721  coe1fv  18798  coe1fzgsumdlem  18894  evl1gsumdlem  18943  zrhmulg  19079  znzrhval  19115  ocvval  19228  mat1dimscm  19498  dmatid  19518  scmatdmat  19538  mavmul0g  19576  1marepvmarrepid  19598  mdetunilem2  19636  gsummatr01lem3  19680  gsummatr01  19682  smadiadetlem3  19691  m2cpminvid2lem  19776  chpdmatlem2  19861  isopn3  20080  cnpval  20250  ptbasfi  20594  dfac14  20631  cnmptkk  20696  xkofvcn  20697  cnmptk1p  20698  cnmptk2  20699  xkocnv  20827  flfval  21003  ptcmplem3  21067  ptcmpg  21070  tmdmulg  21105  prdsxmslem2  21542  subgnm2  21640  nmoval  21718  nmovalOLD  21737  fsum2cn  21901  pcovalg  22041  cphnm  22169  tchnmval  22201  ovolctb  22441  ioorcl  22527  ioorclOLD  22532  uniioombllem2  22538  uniioombllem2OLD  22539  itg1addlem3  22654  itg1climres  22670  itg2uba  22699  itg2splitlem  22704  elcpn  22886  dvexp  22905  dvexp2  22906  rolle  22940  cmvth  22941  mvth  22942  dvlip  22943  dvlipcn  22944  dvlip2  22945  dveq0  22950  dv11cn  22951  lhop1lem  22963  lhop2  22965  lhop  22966  dvcvx  22970  ftc2ditglem  22995  itgsubstlem  22998  ig1pval  23122  ig1pvalOLD  23128  elply2  23148  coeid2  23191  coemul  23204  taylthlem2  23327  ulmdvlem1  23353  mtest  23357  pserval2  23364  abelthlem1  23384  abelthlem3  23386  abelthlem8  23392  abelthlem9  23393  pige3  23470  0cxp  23609  leibpi  23866  igamgam  23972  mule1  24073  bposlem5  24214  lgsval3  24240  lgsdinn0  24266  dchrvmasumlem1  24331  dchrisum0flblem1  24344  rpvmasum2  24348  padicval  24453  axsegconlem1  24945  ax5seglem9  24965  axpasch  24969  axeuclidlem  24990  axcontlem2  24993  nbgraop  25149  nbgraop1  25151  constr1trl  25316  1pthon  25319  2pthlem2  25324  usgra2adedgwlkonALT  25342  constr3pthlem3  25383  wlkiswwlk2lem3  25419  wwlknred  25449  wwlkextproplem2  25468  clwwlkgt0  25497  clwlkisclwwlklem2a  25511  clwwlkf  25520  clwwlkext2edg  25528  wwlkext2clwwlk  25529  clwwisshclwwn  25534  erclwwlknsym  25552  erclwwlkntr  25553  el2spthonot0  25597  vdgrval  25622  extwwlkfablem1  25800  numclwwlkovf2ex  25812  numclwlk1lem2f1  25820  numclwwlk5lem  25837  grpoidinvlem4  25933  grposn  25941  grpoinvval  25951  grpodivval  25969  gxval  25984  gxnn0add  26000  subgoov  26031  ablosn  26073  ipval  26337  sspgval  26366  sspsval  26368  sspnval  26374  nmooval  26402  ipasslem1  26470  ipasslem4  26473  hial0  26753  hial02  26754  ocsh  26934  pjhval  27048  hosval  27391  homval  27392  hodval  27393  hfsval  27394  hfmval  27395  braval  27595  kbval  27605  eigvalval  27611  0hmop  27634  adj0  27645  lnopeq0i  27658  nmopcoi  27746  pjclem4  27850  pj3si  27858  hstoh  27883  strlem3a  27903  hstrlem3a  27911  mdexchi  27986  atcv0eq  28030  atcv1  28031  fpwrelmap  28324  smatfval  28629  measxun2  29040  measdivcstOLD  29054  measdivcst  29055  ddeval1  29065  ddeval0  29066  ballotlemfp1  29332  signswmnd  29454  signstfvneq0  29469  bnj1128  29807  subfacp1lem3  29913  subfacp1lem5  29915  cvmlift2lem3  30036  msubco  30177  altopthsn  30733  fnetr  31012  fnejoin2  31030  finxpreclem3  31749  finxpreclem5  31751  finxpreclem6  31752  poimirlem4  31908  poimirlem25  31929  mblfinlem2  31942  mblfinlem3  31943  mbfresfi  31951  itg2addnclem  31957  itg2addnc  31960  ftc1anclem5  31985  isbnd3  32080  bndss  32082  ghomco  32145  lkrval  32623  pmapval  33291  polvalN  33439  watvalN  33527  ldilset  33643  ltrnset  33652  dilsetN  33688  trnsetN  33691  trlset  33696  trlval  33697  cdleme16b  33814  cdleme31fv1  33927  cdlemg1idlemN  34108  tgrpset  34281  tendoset  34295  erngset  34336  erngplus  34339  erngmul  34342  erngset-rN  34344  erngplus-rN  34347  dvaset  34541  dvaplusg  34545  dvamulr  34548  dvavadd  34551  dvavsca  34553  diafval  34568  dvhset  34618  dvhmulr  34623  dvhvadd  34629  dvhvsca  34638  docafvalN  34659  djafvalN  34671  dibfval  34678  dicfval  34712  dihfval  34768  dihval  34769  dihvalc  34770  dihvalb  34774  dochfval  34887  djhfval  34934  lcdval  35126  mapdfval  35164  mapdn0  35206  hvmapfval  35296  hdmap1fval  35334  hdmapfval  35367  hgmapfval  35426  pw2f1ocnv  35862  hbtlem7  35954  relexp0a  36278  dvconstbi  36653  expgrowth  36654  addrfv  36792  subrfv  36793  mulvfv  36794  refsum2cnlem1  37331  limcperiod  37648  cncfiooiccre  37713  dvbdfbdioolem1  37740  itgioocnicc  37794  fourierdlem73  37983  fourierdlem82  37992  fourierdlem94  38004  fourierdlem103  38013  fourierdlem104  38014  fourierdlem113  38023  sqwvfoura  38032  etransclem46  38085  ovn0  38292  afveu  38525  bgoldbwt  38748  nnsum4primeseven  38765  nnsum4primesevenALTV  38766  bgoldbtbnd  38774  ccats1pfxeqbi  38842  uhgrasiz  39325  lmod0rng  39487  rnghmval  39510  lmodvsmdi  39788  lincdifsn  39838  lcoel0  39842  islindeps2  39897  blenn0  40005  nn0sumshdiglemA  40051  aacllem  40161