Theorem sylan9eq 2258

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198

This theorem is referenced by:  sylan9req  2259  sylan9eqr  2260  difeq12  3286  uneq12  3322  ineq12  3369  ifeq12  3587  preq12  3712  prprc  3743  preq12b  3811  opeq12  3821  xpeq12  4695  nfimad  5032  coi2  5200  funimass1  5352  f1orescnv  5540  resdif  5546  oveq12  5955  cbvmpov  6027  ovmpog  6082  fvmpopr2d  6084  eqopi  6260  fmpoco  6304  nnaordex  6616  map0g  6777  xpcomco  6923  xpmapenlem  6948  phplem3  6953  phplem4  6954  sbthlemi5  7065  addcmpblnq  7482  ltrnqg  7535  enq0ref  7548  addcmpblnq0  7558  distrlem4prl  7699  distrlem4pru  7700  recexgt0sr  7888  axcnre  7996  cnegexlem2  8250  cnegexlem3  8251  recexap  8728  xaddpnf2  9971  xaddmnf2  9973  rexadd  9976  xaddnemnf  9981  xaddnepnf  9982  xposdif  10006  frec2uzrand  10552  seqeq3  10599  seqf1oglem2  10667  seqf1og  10668  lsw1  11045  shftcan1  11178  remul2  11217  immul2  11224  fprodssdc  11934  ef0lem  12004  efieq1re  12116  dvdsnegb  12152  dvdscmul  12162  dvds2ln  12168  dvds2add  12169  dvds2sub  12170  gcdn0val  12315  rpmulgcd  12380  lcmval  12418  lcmn0val  12421  odzval  12597  pcmpt  12699  grpsubval  13411  mulgnn0gsum  13497  crngpropd  13834  opprringbg  13875  dvdsrtr  13896  isopn3  14630  dvexp  15216  dvexp2  15217  elply2  15240  lgsval3  15528  lgsdinn0  15558  subctctexmid  15974