Theorem sylan9eq 2223

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 2188	. 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 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  sylan9req  2224  sylan9eqr  2225  difeq12  3240  uneq12  3276  ineq12  3323  ifeq12  3542  preq12  3662  prprc  3693  preq12b  3757  opeq12  3767  xpeq12  4630  nfimad  4962  coi2  5127  funimass1  5275  f1orescnv  5458  resdif  5464  oveq12  5862  cbvmpov  5933  ovmpog  5987  eqopi  6151  fmpoco  6195  nnaordex  6507  map0g  6666  xpcomco  6804  xpmapenlem  6827  phplem3  6832  phplem4  6833  sbthlemi5  6938  addcmpblnq  7329  ltrnqg  7382  enq0ref  7395  addcmpblnq0  7405  distrlem4prl  7546  distrlem4pru  7547  recexgt0sr  7735  axcnre  7843  cnegexlem2  8095  cnegexlem3  8096  recexap  8571  xaddpnf2  9804  xaddmnf2  9806  rexadd  9809  xaddnemnf  9814  xaddnepnf  9815  xposdif  9839  frec2uzrand  10361  seqeq3  10406  shftcan1  10798  remul2  10837  immul2  10844  fprodssdc  11553  ef0lem  11623  efieq1re  11734  dvdsnegb  11770  dvdscmul  11780  dvds2ln  11786  dvds2add  11787  dvds2sub  11788  gcdn0val  11916  rpmulgcd  11981  lcmval  12017  lcmn0val  12020  odzval  12195  pcmpt  12295  grpsubval  12749  isopn3  12919  dvexp  13469  dvexp2  13470  lgsval3  13713  lgsdinn0  13743  subctctexmid  14034