Theorem sylan9eq 2285

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 2250	. 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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  sylan9req  2286  sylan9eqr  2287  difeq12  3332  uneq12  3368  ineq12  3417  ifeq12  3639  preq12  3770  prprc  3802  preq12b  3874  opeq12  3885  xpeq12  4768  nfimad  5110  coi2  5279  funimass1  5433  f1orescnv  5630  resdif  5636  oveq12  6059  cbvmpov  6133  ovmpog  6188  fvmpopr2d  6190  eqopi  6366  fmpoco  6412  supp0cosupp0fn  6467  imacosuppfn  6468  nnaordex  6761  map0g  6922  xpcomco  7077  xpmapenlem  7102  phplem3  7108  phplem4  7109  sbthlemi5  7231  addcmpblnq  7682  ltrnqg  7735  enq0ref  7748  addcmpblnq0  7758  distrlem4prl  7899  distrlem4pru  7900  recexgt0sr  8088  axcnre  8196  cnegexlem2  8449  cnegexlem3  8450  recexap  8927  xaddpnf2  10180  xaddmnf2  10182  rexadd  10185  xaddnemnf  10190  xaddnepnf  10191  xposdif  10215  frec2uzrand  10767  seqeq3  10814  seqf1oglem2  10882  seqf1og  10883  lsw1  11272  swrdccat  11425  ccats1pfxeqbi  11432  shftcan1  11517  remul2  11556  immul2  11563  fprodssdc  12274  ef0lem  12344  efieq1re  12456  dvdsnegb  12492  dvdscmul  12502  dvds2ln  12508  dvds2add  12509  dvds2sub  12510  gcdn0val  12655  rpmulgcd  12720  lcmval  12758  lcmn0val  12761  odzval  12937  pcmpt  13039  grpsubval  13757  mulgnn0gsum  13843  crngpropd  14181  opprringbg  14222  dvdsrtr  14244  isopn3  14988  dvexp  15574  dvexp2  15575  elply2  15598  lgsval3  15889  lgsdinn0  15919  incistruhgr  16083  clwwlkn1loopb  16413  clwwlkext2edg  16415  clwwlknonex2  16432  eupth2lem3lem3fi  16463  subctctexmid  16772