Theorem sylan9eq 2258

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 2223	. 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 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  sylan9req  2259  sylan9eqr  2260  difeq12  3286  uneq12  3322  ineq12  3369  ifeq12  3587  preq12  3712  prprc  3743  preq12b  3811  opeq12  3821  xpeq12  4694  nfimad  5031  coi2  5199  funimass1  5351  f1orescnv  5538  resdif  5544  oveq12  5953  cbvmpov  6025  ovmpog  6080  fvmpopr2d  6082  eqopi  6258  fmpoco  6302  nnaordex  6614  map0g  6775  xpcomco  6921  xpmapenlem  6946  phplem3  6951  phplem4  6952  sbthlemi5  7063  addcmpblnq  7480  ltrnqg  7533  enq0ref  7546  addcmpblnq0  7556  distrlem4prl  7697  distrlem4pru  7698  recexgt0sr  7886  axcnre  7994  cnegexlem2  8248  cnegexlem3  8249  recexap  8726  xaddpnf2  9969  xaddmnf2  9971  rexadd  9974  xaddnemnf  9979  xaddnepnf  9980  xposdif  10004  frec2uzrand  10550  seqeq3  10597  seqf1oglem2  10665  seqf1og  10666  lsw1  11043  shftcan1  11145  remul2  11184  immul2  11191  fprodssdc  11901  ef0lem  11971  efieq1re  12083  dvdsnegb  12119  dvdscmul  12129  dvds2ln  12135  dvds2add  12136  dvds2sub  12137  gcdn0val  12282  rpmulgcd  12347  lcmval  12385  lcmn0val  12388  odzval  12564  pcmpt  12666  grpsubval  13378  mulgnn0gsum  13464  crngpropd  13801  opprringbg  13842  dvdsrtr  13863  isopn3  14597  dvexp  15183  dvexp2  15184  elply2  15207  lgsval3  15495  lgsdinn0  15525  subctctexmid  15941