Theorem sylan9eq 2525

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 2490	. 2 |- ( ( A = B /\ B = C ) -> A = C )
4	1, 2, 3	syl2an 485	1 |- ( ( ph /\ ps ) -> A = C )

Syntax hints:   -> wi 4   /\ wa 376   = wceq 1452

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-cleq 2464

This theorem is referenced by:  sylan9req  2526  sylan9eqr  2527  difeq12  3535  uneq12  3574  ineq12  3620  ifeq12  3889  ifbi  3893  preq12  4044  prprc  4075  preq12b  4142  opeq12  4160  opthwiener  4703  xpeq12  4858  sosn  4909  nfimad  5183  coi2  5359  ordintdif  5479  funcnvtp  5647  funcnvqp  5648  funimass1  5666  f1orescnv  5843  resdif  5848  fvmpt2  5972  fvmptnf  5982  oveq12  6317  cbvmpt2v  6390  ovmpt2g  6450  caofinvl  6577  eqopi  6846  fmpt2co  6898  mpt2sn  6906  supp0cosupp0  6973  mpt2curryd  7034  fvmpt2curryd  7036  wrecseq123  7047  rdgsucmptf  7164  frsucmpt  7173  oevn0  7235  oa0r  7258  om1r  7262  oe1m  7264  omass  7299  oeoalem  7315  oeoa  7316  oeoe  7318  map0g  7529  xpcomco  7680  sbthlem4  7703  sbthlem5  7704  xpmapenlem  7757  phplem3  7771  phplem4  7772  unxpdomlem3  7796  funsnfsupp  7925  ordtypelem7  8057  cardennn  8435  dfac9  8584  cdaassen  8630  alephsing  8724  axcc3  8886  ac6num  8927  konigthlem  9011  canthp1lem2  9096  ordpipq  9385  ltrnq  9422  addclprlem2  9460  mulclprlem  9462  prlem934  9476  prlem936  9490  mulcmpblnrlem  9512  addcnsr  9577  mulcnsr  9578  axcnre  9606  recex  10266  rpnnen1lem3  11315  rpnnen1lem5  11317  xaddpnf1  11542  xaddpnf2  11543  xaddmnf1  11544  xaddmnf2  11545  rexadd  11548  xaddnemnf  11551  xaddnepnf  11552  xadddilem  11605  addmodlteq  12198  om2uzrani  12204  om2uzrdg  12208  seqf1olem2  12291  seqf1o  12292  modexp  12445  faclbnd4lem3  12518  hashunsng  12609  lsw1  12765  swrdfv  12834  swrdccat  12903  ccats1swrdeqbi  12908  revfv  12922  cshwsublen  12952  wrdlen2  13095  wrdl2exs2  13097  wwlktovf1  13107  relexp0  13163  relexpcnv  13175  shftcan1  13223  remul2  13270  immul2  13277  sumss  13867  geomulcvg  14009  fprodss  14079  binomfallfaclem2  14170  bpolylem  14178  ef0lem  14210  efieq1re  14330  rpnnen2lem1  14344  ruclem3  14362  dvdsnegb  14397  dvdscmul  14406  dvds2ln  14410  dvds2add  14411  dvds2sub  14412  gcdn0val  14551  rpmulgcd  14602  lcmn0val  14638  lcmn0valOLD  14639  odzval  14815  odzvalOLD  14821  pcval  14873  pcmpt  14916  prmreclem4  14942  1arithlem2  14947  vdwlem8  15017  ramcl2lem  15041  ramcl2lemOLD  15042  ramtcl  15043  ramtclOLD  15044  ramtub  15047  ramtubOLD  15048  ramcl2  15052  ramcl2OLD  15053  ramcl  15066  setsval  15224  prfcl  16166  curf1cl  16191  curfcl  16195  hofcl  16222  yonedalem4c  16240  psssdm  16540  grplactval  16831  cntzval  17053  f1omvdco2  17167  pmtrfinv  17180  psgnunilem5  17213  odlem2  17266  odlem2OLD  17282  gexlem2  17311  gexlem2OLD  17314  lsmvalx  17369  efgtval  17451  efgredlema  17468  vrgpval  17495  cyggex  17610  gsumcom2  17685  dvdsrtr  17958  abvtrivd  18146  lmhmco  18344  reslmhm  18353  lvecinv  18414  mplmon2  18793  subrgasclcl  18799  coe1fv  18876  coe1fzgsumdlem  18972  evl1gsumdlem  19021  zrhmulg  19158  znzrhval  19194  ocvval  19307  mat1dimscm  19577  dmatid  19597  scmatdmat  19617  mavmul0g  19655  1marepvmarrepid  19677  mdetunilem2  19715  gsummatr01lem3  19759  gsummatr01  19761  smadiadetlem3  19770  m2cpminvid2lem  19855  chpdmatlem2  19940  isopn3  20159  cnpval  20329  ptbasfi  20673  dfac14  20710  cnmptkk  20775  xkofvcn  20776  cnmptk1p  20777  cnmptk2  20778  xkocnv  20906  flfval  21083  ptcmplem3  21147  ptcmpg  21150  tmdmulg  21185  prdsxmslem2  21622  subgnm2  21720  nmoval  21798  nmovalOLD  21817  fsum2cn  21981  pcovalg  22121  cphnm  22249  tchnmval  22281  ovolctb  22521  ioorcl  22608  ioorclOLD  22613  uniioombllem2  22619  uniioombllem2OLD  22620  itg1addlem3  22735  itg1climres  22751  itg2uba  22780  itg2splitlem  22785  elcpn  22967  dvexp  22986  dvexp2  22987  rolle  23021  cmvth  23022  mvth  23023  dvlip  23024  dvlipcn  23025  dvlip2  23026  dveq0  23031  dv11cn  23032  lhop1lem  23044  lhop2  23046  lhop  23047  dvcvx  23051  ftc2ditglem  23076  itgsubstlem  23079  ig1pval  23203  ig1pvalOLD  23209  elply2  23229  coeid2  23272  coemul  23285  taylthlem2  23408  ulmdvlem1  23434  mtest  23438  pserval2  23445  abelthlem1  23465  abelthlem3  23467  abelthlem8  23473  abelthlem9  23474  pige3  23551  0cxp  23690  leibpi  23947  igamgam  24053  mule1  24154  bposlem5  24295  lgsval3  24321  lgsdinn0  24347  dchrvmasumlem1  24412  dchrisum0flblem1  24425  rpvmasum2  24429  padicval  24534  axsegconlem1  25026  ax5seglem9  25046  axpasch  25050  axeuclidlem  25071  axcontlem2  25074  nbgraop  25230  nbgraop1  25232  constr1trl  25397  1pthon  25400  2pthlem2  25405  usgra2adedgwlkonALT  25423  constr3pthlem3  25464  wlkiswwlk2lem3  25500  wwlknred  25530  wwlkextproplem2  25549  clwwlkgt0  25578  clwlkisclwwlklem2a  25592  clwwlkf  25601  clwwlkext2edg  25609  wwlkext2clwwlk  25610  clwwisshclwwn  25615  erclwwlknsym  25633  erclwwlkntr  25634  el2spthonot0  25678  vdgrval  25703  extwwlkfablem1  25881  numclwwlkovf2ex  25893  numclwlk1lem2f1  25901  numclwwlk5lem  25918  grpoidinvlem4  26016  grposn  26024  grpoinvval  26034  grpodivval  26052  gxval  26067  gxnn0add  26083  subgoov  26114  ablosn  26156  ipval  26420  sspgval  26449  sspsval  26451  sspnval  26457  nmooval  26485  ipasslem1  26553  ipasslem4  26556  hial0  26836  hial02  26837  ocsh  27017  pjhval  27131  hosval  27474  homval  27475  hodval  27476  hfsval  27477  hfmval  27478  braval  27678  kbval  27688  eigvalval  27694  0hmop  27717  adj0  27728  lnopeq0i  27741  nmopcoi  27829  pjclem4  27933  pj3si  27941  hstoh  27966  strlem3a  27986  hstrlem3a  27994  mdexchi  28069  atcv0eq  28113  atcv1  28114  fpwrelmap  28393  smatfval  28695  measxun2  29106  measdivcstOLD  29120  measdivcst  29121  ddeval1  29130  ddeval0  29131  ballotlemfp1  29397  signswmnd  29518  signstfvneq0  29533  bnj1128  29871  subfacp1lem3  29977  subfacp1lem5  29979  cvmlift2lem3  30100  msubco  30241  altopthsn  30799  fnetr  31078  fnejoin2  31096  finxpreclem3  31855  finxpreclem5  31857  finxpreclem6  31858  poimirlem4  32008  poimirlem25  32029  mblfinlem2  32042  mblfinlem3  32043  mbfresfi  32051  itg2addnclem  32057  itg2addnc  32060  ftc1anclem5  32085  isbnd3  32180  bndss  32182  ghomco  32245  lkrval  32725  pmapval  33393  polvalN  33541  watvalN  33629  ldilset  33745  ltrnset  33754  dilsetN  33790  trnsetN  33793  trlset  33798  trlval  33799  cdleme16b  33916  cdleme31fv1  34029  cdlemg1idlemN  34210  tgrpset  34383  tendoset  34397  erngset  34438  erngplus  34441  erngmul  34444  erngset-rN  34446  erngplus-rN  34449  dvaset  34643  dvaplusg  34647  dvamulr  34650  dvavadd  34653  dvavsca  34655  diafval  34670  dvhset  34720  dvhmulr  34725  dvhvadd  34731  dvhvsca  34740  docafvalN  34761  djafvalN  34773  dibfval  34780  dicfval  34814  dihfval  34870  dihval  34871  dihvalc  34872  dihvalb  34876  dochfval  34989  djhfval  35036  lcdval  35228  mapdfval  35266  mapdn0  35308  hvmapfval  35398  hdmap1fval  35436  hdmapfval  35469  hgmapfval  35528  pw2f1ocnv  35963  hbtlem7  36055  relexp0a  36379  dvconstbi  36753  expgrowth  36754  addrfv  36892  subrfv  36893  mulvfv  36894  refsum2cnlem1  37421  limcperiod  37805  cncfiooiccre  37870  dvbdfbdioolem1  37897  itgioocnicc  37951  fourierdlem73  38155  fourierdlem82  38164  fourierdlem94  38176  fourierdlem103  38185  fourierdlem104  38186  fourierdlem113  38195  sqwvfoura  38204  etransclem46  38257  ovn0  38506  afveu  38800  bgoldbwt  39023  nnsum4primeseven  39040  nnsum4primesevenALTV  39041  bgoldbtbnd  39049  ccats1pfxeqbi  39119  xnn0xaddcl  39236  crctcshlem4  39998  eupth2lem3lem3  40142  eucrct2eupth  40157  uhgrasiz  40214  lmod0rng  40376  rnghmval  40399  lmodvsmdi  40675  lincdifsn  40725  lcoel0  40729  islindeps2  40784  blenn0  40892  nn0sumshdiglemA  40938  aacllem  41046