Theorem sylan9eq 2284

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 2249	. 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 2213

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

This theorem is referenced by:  sylan9req  2285  sylan9eqr  2286  difeq12  3322  uneq12  3358  ineq12  3405  ifeq12  3626  preq12  3754  prprc  3786  preq12b  3858  opeq12  3869  xpeq12  4750  nfimad  5091  coi2  5260  funimass1  5414  f1orescnv  5608  resdif  5614  oveq12  6037  cbvmpov  6111  ovmpog  6166  fvmpopr2d  6168  eqopi  6344  fmpoco  6390  supp0cosupp0fn  6445  imacosuppfn  6446  nnaordex  6739  map0g  6900  xpcomco  7053  xpmapenlem  7078  phplem3  7083  phplem4  7084  sbthlemi5  7203  addcmpblnq  7647  ltrnqg  7700  enq0ref  7713  addcmpblnq0  7723  distrlem4prl  7864  distrlem4pru  7865  recexgt0sr  8053  axcnre  8161  cnegexlem2  8414  cnegexlem3  8415  recexap  8892  xaddpnf2  10143  xaddmnf2  10145  rexadd  10148  xaddnemnf  10153  xaddnepnf  10154  xposdif  10178  frec2uzrand  10730  seqeq3  10777  seqf1oglem2  10845  seqf1og  10846  lsw1  11229  swrdccat  11382  ccats1pfxeqbi  11389  shftcan1  11474  remul2  11513  immul2  11520  fprodssdc  12231  ef0lem  12301  efieq1re  12413  dvdsnegb  12449  dvdscmul  12459  dvds2ln  12465  dvds2add  12466  dvds2sub  12467  gcdn0val  12612  rpmulgcd  12677  lcmval  12715  lcmn0val  12718  odzval  12894  pcmpt  12996  grpsubval  13709  mulgnn0gsum  13795  crngpropd  14133  opprringbg  14174  dvdsrtr  14196  isopn3  14936  dvexp  15522  dvexp2  15523  elply2  15546  lgsval3  15837  lgsdinn0  15867  incistruhgr  16031  clwwlkn1loopb  16361  clwwlkext2edg  16363  clwwlknonex2  16380  eupth2lem3lem3fi  16411  subctctexmid  16722