Theorem sylan9eq 2230

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

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  sylan9req  2231  sylan9eqr  2232  difeq12  3250  uneq12  3286  ineq12  3333  ifeq12  3552  preq12  3673  prprc  3704  preq12b  3772  opeq12  3782  xpeq12  4647  nfimad  4981  coi2  5147  funimass1  5295  f1orescnv  5479  resdif  5485  oveq12  5886  cbvmpov  5957  ovmpog  6011  eqopi  6175  fmpoco  6219  nnaordex  6531  map0g  6690  xpcomco  6828  xpmapenlem  6851  phplem3  6856  phplem4  6857  sbthlemi5  6962  addcmpblnq  7368  ltrnqg  7421  enq0ref  7434  addcmpblnq0  7444  distrlem4prl  7585  distrlem4pru  7586  recexgt0sr  7774  axcnre  7882  cnegexlem2  8135  cnegexlem3  8136  recexap  8612  xaddpnf2  9849  xaddmnf2  9851  rexadd  9854  xaddnemnf  9859  xaddnepnf  9860  xposdif  9884  frec2uzrand  10407  seqeq3  10452  shftcan1  10845  remul2  10884  immul2  10891  fprodssdc  11600  ef0lem  11670  efieq1re  11781  dvdsnegb  11817  dvdscmul  11827  dvds2ln  11833  dvds2add  11834  dvds2sub  11835  gcdn0val  11964  rpmulgcd  12029  lcmval  12065  lcmn0val  12068  odzval  12243  pcmpt  12343  grpsubval  12924  crngpropd  13223  opprringbg  13255  dvdsrtr  13275  isopn3  13710  dvexp  14260  dvexp2  14261  lgsval3  14504  lgsdinn0  14534  subctctexmid  14835