Theorem sylan9eq 2217

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 2182	. 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 1342

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 1434  ax-gen 1436  ax-4 1497  ax-17 1513  ax-ext 2146

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

This theorem is referenced by:  sylan9req  2218  sylan9eqr  2219  difeq12  3230  uneq12  3266  ineq12  3313  ifeq12  3531  preq12  3649  prprc  3680  preq12b  3744  opeq12  3754  xpeq12  4617  nfimad  4949  coi2  5114  funimass1  5259  f1orescnv  5442  resdif  5448  oveq12  5845  cbvmpov  5913  ovmpog  5967  eqopi  6132  fmpoco  6175  nnaordex  6486  map0g  6645  xpcomco  6783  xpmapenlem  6806  phplem3  6811  phplem4  6812  sbthlemi5  6917  addcmpblnq  7299  ltrnqg  7352  enq0ref  7365  addcmpblnq0  7375  distrlem4prl  7516  distrlem4pru  7517  recexgt0sr  7705  axcnre  7813  cnegexlem2  8065  cnegexlem3  8066  recexap  8541  xaddpnf2  9774  xaddmnf2  9776  rexadd  9779  xaddnemnf  9784  xaddnepnf  9785  xposdif  9809  frec2uzrand  10330  seqeq3  10375  shftcan1  10762  remul2  10801  immul2  10808  fprodssdc  11517  ef0lem  11587  efieq1re  11698  dvdsnegb  11734  dvdscmul  11744  dvds2ln  11750  dvds2add  11751  dvds2sub  11752  gcdn0val  11879  rpmulgcd  11944  lcmval  11974  lcmn0val  11977  odzval  12150  pcmpt  12250  isopn3  12666  dvexp  13216  dvexp2  13217  subctctexmid  13715