Theorem sylan9eq 2528

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459

This theorem is referenced by:  sylan9req  2529  sylan9eqr  2530  difeq12  3617  uneq12  3653  ineq12  3695  ifeq12  3956  ifbi  3960  preq12  4108  prprc  4139  preq12b  4202  opeq12  4215  opthwiener  4749  ordintdif  4927  xpeq12  5018  sosn  5069  nfimad  5346  coi2  5524  funimass1  5661  f1orescnv  5831  resdif  5836  fvmpt2  5957  fvmptnf  5967  oveq12  6293  cbvmpt2v  6361  ovmpt2g  6421  caofinvl  6551  eqopi  6818  fmpt2co  6866  mpt2sn  6874  supp0cosupp0  6939  mpt2curryd  6998  fvmpt2curryd  7000  rdgsucmptf  7094  frsucmpt  7103  oevn0  7165  oa0r  7188  om1r  7192  oe1m  7194  omass  7229  oeoalem  7245  oeoa  7246  oeoe  7248  map0g  7458  xpcomco  7607  sbthlem4  7630  sbthlem5  7631  xpmapenlem  7684  phplem3  7698  phplem4  7699  unxpdomlem3  7726  funsnfsupp  7853  ordtypelem7  7949  cardennn  8364  dfac9  8516  cdaassen  8562  alephsing  8656  axcc3  8818  ac6num  8859  konigthlem  8943  canthp1lem2  9031  ordpipq  9320  ltrnq  9357  addclprlem2  9395  mulclprlem  9397  prlem934  9411  prlem936  9425  mulcmpblnrlem  9447  addcnsr  9512  mulcnsr  9513  axcnre  9541  recex  10181  uzindOLD  10955  rpnnen1lem3  11210  rpnnen1lem5  11212  xaddpnf1  11425  xaddpnf2  11426  xaddmnf1  11427  xaddmnf2  11428  rexadd  11431  xaddnemnf  11433  xaddnepnf  11434  xadddilem  11486  om2uzrani  12031  om2uzrdg  12035  seqf1olem2  12115  seqf1o  12116  modexp  12269  faclbnd4lem3  12341  hashunsng  12427  lsw1  12553  ccatw2s1p1  12603  ccatw2s1p2  12604  swrdfv  12614  swrdccat  12681  ccats1swrdeqbi  12686  revfv  12700  cshwsublen  12730  wrdlen2  12849  wwlktovf1  12858  shftcan1  12879  remul2  12926  immul2  12933  sumss  13509  geomulcvg  13648  ef0lem  13676  efieq1re  13795  rpnnen2lem1  13809  ruclem3  13827  dvdsnegb  13862  dvdscmul  13871  dvds2ln  13875  dvds2add  13876  dvds2sub  13877  gcdn0val  14007  rpmulgcd  14052  odzval  14177  pcval  14227  pcmpt  14270  prmreclem4  14296  1arithlem2  14301  vdwlem8  14365  ramcl2lem  14386  ramtcl  14387  ramtub  14389  ramcl2  14393  ramcl  14406  setsval  14514  prfcl  15330  curf1cl  15355  curfcl  15359  hofcl  15386  yonedalem4c  15404  psssdm  15703  grplactval  15947  cntzval  16164  f1omvdco2  16279  pmtrfinv  16292  odlem2  16369  gexlem2  16408  lsmvalx  16465  efgtval  16547  efgredlema  16564  vrgpval  16591  cyggex  16703  gsumcom2  16806  dvdsrtr  17102  abvtrivd  17289  lmhmco  17489  reslmhm  17498  lvecinv  17559  mplmon2  17957  subrgasclcl  17963  coe1fv  18044  coe1fzgsumdlem  18142  evl1gsumdlem  18191  zrhmulg  18342  znzrhval  18380  ocvval  18493  mat1dimscm  18772  dmatid  18792  scmatdmat  18812  mavmul0g  18850  1marepvmarrepid  18872  mdetunilem2  18910  gsummatr01lem3  18954  gsummatr01  18956  smadiadetlem3  18965  m2cpminvid2lem  19050  chpdmatlem2  19135  isopn3  19361  cnpval  19531  ptbasfi  19845  dfac14  19882  cnmptkk  19947  xkofvcn  19948  cnmptk1p  19949  cnmptk2  19950  xkocnv  20078  flfval  20254  ptcmplem3  20317  ptcmpg  20320  tmdmulg  20354  prdsxmslem2  20795  subgnm2  20911  nmoval  20985  fsum2cn  21138  pcovalg  21275  cphnm  21403  tchnmval  21435  ovolctb  21664  ioorcl  21749  uniioombllem2  21755  itg1addlem3  21868  itg1climres  21884  itg2uba  21913  itg2splitlem  21918  elcpn  22100  dvexp  22119  dvexp2  22120  rolle  22154  cmvth  22155  mvth  22156  dvlip  22157  dvlipcn  22158  dvlip2  22159  dveq0  22164  dv11cn  22165  lhop1lem  22177  lhop2  22179  lhop  22180  dvcvx  22184  ftc2ditglem  22209  itgsubstlem  22212  ig1pval  22336  elply2  22356  coeid2  22399  coemul  22411  taylthlem2  22531  ulmdvlem1  22557  mtest  22561  pserval2  22568  abelthlem1  22588  abelthlem3  22590  abelthlem8  22596  abelthlem9  22597  pige3  22671  0cxp  22803  leibpi  23029  mule1  23178  bposlem5  23319  lgsval3  23345  lgsdinn0  23371  dchrvmasumlem1  23436  dchrisum0flblem1  23449  rpvmasum2  23453  padicval  23558  axsegconlem1  23924  ax5seglem9  23944  axpasch  23948  axeuclidlem  23969  axcontlem2  23972  nbgraop  24127  nbgraop1  24129  constr1trl  24294  1pthon  24297  2pthlem2  24302  usgra2adedgwlkonALT  24320  constr3pthlem3  24361  wlkiswwlk2lem3  24397  wwlknred  24427  wwlkextproplem2  24446  clwwlkgt0  24475  clwlkisclwwlklem2a  24489  clwwlkf  24498  clwwlkext2edg  24506  wwlkext2clwwlk  24507  clwwisshclwwn  24512  erclwwlknsym  24530  erclwwlkntr  24531  el2spthonot0  24575  vdgrval  24600  extwwlkfablem1  24779  numclwwlkovf2ex  24791  numclwlk1lem2f1  24799  numclwwlk5lem  24816  grpoidinvlem4  24913  grposn  24921  grpoinvval  24931  grpodivval  24949  gxval  24964  gxnn0add  24980  subgoov  25011  ablosn  25053  ipval  25317  sspgval  25346  sspsval  25348  sspnval  25354  nmooval  25382  ipasslem1  25450  ipasslem4  25453  hial0  25723  hial02  25724  ocsh  25905  pjhval  26019  hosval  26363  homval  26364  hodval  26365  hfsval  26366  hfmval  26367  braval  26567  kbval  26577  eigvalval  26583  0hmop  26606  adj0  26617  lnopeq0i  26630  nmopcoi  26718  pjclem4  26822  pj3si  26830  hstoh  26855  strlem3a  26875  hstrlem3a  26883  mdexchi  26958  atcv0eq  27002  atcv1  27003  fpwrelmap  27256  measxun2  27849  measdivcstOLD  27863  measdivcst  27864  ddeval1  27874  ddeval0  27875  ballotlemfp1  28098  signswmnd  28182  signstfvneq0  28197  igamgam  28259  subfacp1lem3  28294  subfacp1lem5  28296  cvmlift2lem3  28418  relexp1  28557  relexpcnv  28559  relexpadd  28564  fprodss  28685  binomfallfaclem2  28767  wrecseq123  28942  altopthsn  29216  bpolylem  29415  mblfinlem2  29657  mblfinlem3  29658  mbfresfi  29666  itg2addnclem  29671  itg2addnc  29674  ftc1anclem5  29699  fnetr  29786  reftr  29789  fnejoin2  29818  isbnd3  29911  bndss  29913  ghomco  29976  pw2f1ocnv  30611  hbtlem7  30706  lcmn0val  30829  dvconstbi  30867  expgrowth  30868  addrfv  30984  subrfv  30985  mulvfv  30986  refsum2cnlem1  31018  fourierdlem103  31538  fourierdlem104  31539  afveu  31733  uhgrasiz  31889  lmod0rng  32058  lmodvsmdi  32074  lincdifsn  32124  lcoel0  32128  islindeps2  32183  bnj1128  33143  lkrval  33903  pmapval  34571  polvalN  34719  watvalN  34807  ldilset  34923  ltrnset  34932  dilsetN  34967  trnsetN  34970  trlset  34975  trlval  34976  cdleme16b  35093  cdleme31fv1  35205  cdlemg1idlemN  35386  tgrpset  35559  tendoset  35573  erngset  35614  erngplus  35617  erngmul  35620  erngset-rN  35622  erngplus-rN  35625  dvaset  35819  dvaplusg  35823  dvamulr  35826  dvavadd  35829  dvavsca  35831  diafval  35846  dvhset  35896  dvhmulr  35901  dvhvadd  35907  dvhvsca  35916  docafvalN  35937  djafvalN  35949  dibfval  35956  dicfval  35990  dihfval  36046  dihval  36047  dihvalc  36048  dihvalb  36052  dochfval  36165  djhfval  36212  lcdval  36404  mapdfval  36442  mapdn0  36484  hvmapfval  36574  hdmap1fval  36612  hdmapfval  36645  hgmapfval  36704