Theorem sylan9eq 2249

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 2214	. 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 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  sylan9req  2250  sylan9eqr  2251  difeq12  3277  uneq12  3313  ineq12  3360  ifeq12  3578  preq12  3702  prprc  3733  preq12b  3801  opeq12  3811  xpeq12  4683  nfimad  5019  coi2  5187  funimass1  5336  f1orescnv  5523  resdif  5529  oveq12  5934  cbvmpov  6006  ovmpog  6061  fvmpopr2d  6063  eqopi  6239  fmpoco  6283  nnaordex  6595  map0g  6756  xpcomco  6894  xpmapenlem  6919  phplem3  6924  phplem4  6925  sbthlemi5  7036  addcmpblnq  7451  ltrnqg  7504  enq0ref  7517  addcmpblnq0  7527  distrlem4prl  7668  distrlem4pru  7669  recexgt0sr  7857  axcnre  7965  cnegexlem2  8219  cnegexlem3  8220  recexap  8697  xaddpnf2  9939  xaddmnf2  9941  rexadd  9944  xaddnemnf  9949  xaddnepnf  9950  xposdif  9974  frec2uzrand  10514  seqeq3  10561  seqf1oglem2  10629  seqf1og  10630  shftcan1  11016  remul2  11055  immul2  11062  fprodssdc  11772  ef0lem  11842  efieq1re  11954  dvdsnegb  11990  dvdscmul  12000  dvds2ln  12006  dvds2add  12007  dvds2sub  12008  gcdn0val  12153  rpmulgcd  12218  lcmval  12256  lcmn0val  12259  odzval  12435  pcmpt  12537  grpsubval  13248  mulgnn0gsum  13334  crngpropd  13671  opprringbg  13712  dvdsrtr  13733  isopn3  14445  dvexp  15031  dvexp2  15032  elply2  15055  lgsval3  15343  lgsdinn0  15373  subctctexmid  15731