Theorem sylan9eq 2246

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 2211	. 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 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  sylan9req  2247  sylan9eqr  2248  difeq12  3273  uneq12  3309  ineq12  3356  ifeq12  3574  preq12  3698  prprc  3729  preq12b  3797  opeq12  3807  xpeq12  4679  nfimad  5015  coi2  5183  funimass1  5332  f1orescnv  5517  resdif  5523  oveq12  5928  cbvmpov  5999  ovmpog  6054  fvmpopr2d  6056  eqopi  6227  fmpoco  6271  nnaordex  6583  map0g  6744  xpcomco  6882  xpmapenlem  6907  phplem3  6912  phplem4  6913  sbthlemi5  7022  addcmpblnq  7429  ltrnqg  7482  enq0ref  7495  addcmpblnq0  7505  distrlem4prl  7646  distrlem4pru  7647  recexgt0sr  7835  axcnre  7943  cnegexlem2  8197  cnegexlem3  8198  recexap  8674  xaddpnf2  9916  xaddmnf2  9918  rexadd  9921  xaddnemnf  9926  xaddnepnf  9927  xposdif  9951  frec2uzrand  10479  seqeq3  10526  seqf1oglem2  10594  seqf1og  10595  shftcan1  10981  remul2  11020  immul2  11027  fprodssdc  11736  ef0lem  11806  efieq1re  11918  dvdsnegb  11954  dvdscmul  11964  dvds2ln  11970  dvds2add  11971  dvds2sub  11972  gcdn0val  12101  rpmulgcd  12166  lcmval  12204  lcmn0val  12207  odzval  12382  pcmpt  12484  grpsubval  13121  mulgnn0gsum  13201  crngpropd  13538  opprringbg  13579  dvdsrtr  13600  isopn3  14304  dvexp  14890  dvexp2  14891  elply2  14914  lgsval3  15175  lgsdinn0  15205  subctctexmid  15561