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  3248  uneq12  3284  ineq12  3331  ifeq12  3550  preq12  3671  prprc  3702  preq12b  3769  opeq12  3779  xpeq12  4643  nfimad  4976  coi2  5142  funimass1  5290  f1orescnv  5474  resdif  5480  oveq12  5879  cbvmpov  5950  ovmpog  6004  eqopi  6168  fmpoco  6212  nnaordex  6524  map0g  6683  xpcomco  6821  xpmapenlem  6844  phplem3  6849  phplem4  6850  sbthlemi5  6955  addcmpblnq  7361  ltrnqg  7414  enq0ref  7427  addcmpblnq0  7437  distrlem4prl  7578  distrlem4pru  7579  recexgt0sr  7767  axcnre  7875  cnegexlem2  8127  cnegexlem3  8128  recexap  8604  xaddpnf2  9841  xaddmnf2  9843  rexadd  9846  xaddnemnf  9851  xaddnepnf  9852  xposdif  9876  frec2uzrand  10398  seqeq3  10443  shftcan1  10834  remul2  10873  immul2  10880  fprodssdc  11589  ef0lem  11659  efieq1re  11770  dvdsnegb  11806  dvdscmul  11816  dvds2ln  11822  dvds2add  11823  dvds2sub  11824  gcdn0val  11952  rpmulgcd  12017  lcmval  12053  lcmn0val  12056  odzval  12231  pcmpt  12331  grpsubval  12847  crngpropd  13118  opprringbg  13149  dvdsrtr  13169  isopn3  13407  dvexp  13957  dvexp2  13958  lgsval3  14201  lgsdinn0  14231  subctctexmid  14521