Theorem sylan9eq 2092

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

Syntax hints:   -> wi 4   /\ wa 97   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  sylan9req  2093  sylan9eqr  2094  difeq12  3057  uneq12  3092  ineq12  3133  ifeq12  3344  preq12  3449  prprc  3480  preq12b  3541  opeq12  3551  xpeq12  4364  nfimad  4677  coi2  4837  funimass1  4976  f1orescnv  5142  resdif  5148  oveq12  5521  cbvmpt2v  5584  ovmpt2g  5635  eqopi  5798  fmpt2co  5837  nnaordex  6100  xpcomco  6300  phplem3  6317  phplem4  6318  addcmpblnq  6465  ltrnqg  6518  enq0ref  6531  addcmpblnq0  6541  distrlem4prl  6682  distrlem4pru  6683  recexgt0sr  6858  axcnre  6955  cnegexlem2  7187  cnegexlem3  7188  recexap  7634  frec2uzzd  9186  frec2uzrand  9191  iseqeq3  9216  shftcan1  9435  remul2  9473  immul2  9480