Theorem sylan9eq 2133

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

Syntax hints:   -> wi 4   /\ wa 102   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  sylan9req  2134  sylan9eqr  2135  difeq12  3085  uneq12  3121  ineq12  3162  ifeq12  3365  preq12  3471  prprc  3502  preq12b  3562  opeq12  3572  xpeq12  4382  nfimad  4697  coi2  4857  funimass1  4996  f1orescnv  5162  resdif  5168  oveq12  5541  cbvmpt2v  5604  ovmpt2g  5655  eqopi  5818  fmpt2co  5857  nnaordex  6123  xpcomco  6323  phplem3  6340  phplem4  6341  addcmpblnq  6557  ltrnqg  6610  enq0ref  6623  addcmpblnq0  6633  distrlem4prl  6774  distrlem4pru  6775  recexgt0sr  6950  axcnre  7047  cnegexlem2  7284  cnegexlem3  7285  recexap  7743  frec2uzzd  9402  frec2uzrand  9407  iseqeq3  9436  shftcan1  9722  remul2  9760  immul2  9767  dvdsnegb  10212  dvdscmul  10222  dvds2ln  10228  dvds2add  10229  dvds2sub  10230  gcdn0val  10353  rpmulgcd  10415  lcmval  10445  lcmn0val  10448