Theorem sylan9eq 2140

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 2105	. 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 1289

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 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070

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

This theorem is referenced by:  sylan9req  2141  sylan9eqr  2142  difeq12  3113  uneq12  3149  ineq12  3196  ifeq12  3407  preq12  3521  prprc  3552  preq12b  3614  opeq12  3624  xpeq12  4457  nfimad  4783  coi2  4947  funimass1  5091  f1orescnv  5269  resdif  5275  oveq12  5661  cbvmpt2v  5728  ovmpt2g  5779  eqopi  5942  fmpt2co  5981  nnaordex  6284  map0g  6443  xpcomco  6540  xpmapenlem  6563  phplem3  6568  phplem4  6569  sbthlemi5  6668  addcmpblnq  6924  ltrnqg  6977  enq0ref  6990  addcmpblnq0  7000  distrlem4prl  7141  distrlem4pru  7142  recexgt0sr  7317  axcnre  7414  cnegexlem2  7656  cnegexlem3  7657  recexap  8120  frec2uzrand  9808  iseqeq3  9856  shftcan1  10264  remul2  10303  immul2  10310  ef0lem  10946  efieq1re  11057  dvdsnegb  11087  dvdscmul  11097  dvds2ln  11103  dvds2add  11104  dvds2sub  11105  gcdn0val  11227  rpmulgcd  11289  lcmval  11319  lcmn0val  11322