Theorem sylan9eq 2192

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

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  sylan9req  2193  sylan9eqr  2194  difeq12  3189  uneq12  3225  ineq12  3272  ifeq12  3488  preq12  3602  prprc  3633  preq12b  3697  opeq12  3707  xpeq12  4558  nfimad  4890  coi2  5055  funimass1  5200  f1orescnv  5383  resdif  5389  oveq12  5783  cbvmpov  5851  ovmpog  5905  eqopi  6070  fmpoco  6113  nnaordex  6423  map0g  6582  xpcomco  6720  xpmapenlem  6743  phplem3  6748  phplem4  6749  sbthlemi5  6849  addcmpblnq  7175  ltrnqg  7228  enq0ref  7241  addcmpblnq0  7251  distrlem4prl  7392  distrlem4pru  7393  recexgt0sr  7581  axcnre  7689  cnegexlem2  7938  cnegexlem3  7939  recexap  8414  xaddpnf2  9630  xaddmnf2  9632  rexadd  9635  xaddnemnf  9640  xaddnepnf  9641  xposdif  9665  frec2uzrand  10178  seqeq3  10223  shftcan1  10606  remul2  10645  immul2  10652  ef0lem  11366  efieq1re  11478  dvdsnegb  11510  dvdscmul  11520  dvds2ln  11526  dvds2add  11527  dvds2sub  11528  gcdn0val  11650  rpmulgcd  11714  lcmval  11744  lcmn0val  11747  isopn3  12294  dvexp  12844  dvexp2  12845  subctctexmid  13196