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  3541  preq12  3660  prprc  3691  preq12b  3755  opeq12  3765  xpeq12  4628  nfimad  4960  coi2  5125  funimass1  5273  f1orescnv  5456  resdif  5462  oveq12  5859  cbvmpov  5930  ovmpog  5984  eqopi  6148  fmpoco  6192  nnaordex  6503  map0g  6662  xpcomco  6800  xpmapenlem  6823  phplem3  6828  phplem4  6829  sbthlemi5  6934  addcmpblnq  7316  ltrnqg  7369  enq0ref  7382  addcmpblnq0  7392  distrlem4prl  7533  distrlem4pru  7534  recexgt0sr  7722  axcnre  7830  cnegexlem2  8082  cnegexlem3  8083  recexap  8558  xaddpnf2  9791  xaddmnf2  9793  rexadd  9796  xaddnemnf  9801  xaddnepnf  9802  xposdif  9826  frec2uzrand  10348  seqeq3  10393  shftcan1  10785  remul2  10824  immul2  10831  fprodssdc  11540  ef0lem  11610  efieq1re  11721  dvdsnegb  11757  dvdscmul  11767  dvds2ln  11773  dvds2add  11774  dvds2sub  11775  gcdn0val  11903  rpmulgcd  11968  lcmval  12004  lcmn0val  12007  odzval  12182  pcmpt  12282  isopn3  12878  dvexp  13428  dvexp2  13429  lgsval3  13672  lgsdinn0  13702  subctctexmid  13994