Theorem sylan9eq 2190

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 2155	. 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 2119

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

This theorem is referenced by:  sylan9req  2191  sylan9eqr  2192  difeq12  3184  uneq12  3220  ineq12  3267  ifeq12  3483  preq12  3597  prprc  3628  preq12b  3692  opeq12  3702  xpeq12  4553  nfimad  4885  coi2  5050  funimass1  5195  f1orescnv  5376  resdif  5382  oveq12  5776  cbvmpov  5844  ovmpog  5898  eqopi  6063  fmpoco  6106  nnaordex  6416  map0g  6575  xpcomco  6713  xpmapenlem  6736  phplem3  6741  phplem4  6742  sbthlemi5  6842  addcmpblnq  7168  ltrnqg  7221  enq0ref  7234  addcmpblnq0  7244  distrlem4prl  7385  distrlem4pru  7386  recexgt0sr  7574  axcnre  7682  cnegexlem2  7931  cnegexlem3  7932  recexap  8407  xaddpnf2  9623  xaddmnf2  9625  rexadd  9628  xaddnemnf  9633  xaddnepnf  9634  xposdif  9658  frec2uzrand  10171  seqeq3  10216  shftcan1  10599  remul2  10638  immul2  10645  ef0lem  11355  efieq1re  11467  dvdsnegb  11499  dvdscmul  11509  dvds2ln  11515  dvds2add  11516  dvds2sub  11517  gcdn0val  11639  rpmulgcd  11703  lcmval  11733  lcmn0val  11736  isopn3  12283  dvexp  12833  dvexp2  12834  subctctexmid  13185