Theorem sylan9eq 2291

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 2256	. 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 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  sylan9req  2292  sylan9eqr  2293  difeq12  3342  uneq12  3378  ineq12  3427  ifeq12  3654  preq12  3786  prprc  3818  preq12b  3890  opeq12  3901  xpeq12  4788  nfimad  5130  coi2  5299  funimass1  5453  f1orescnv  5650  resdif  5656  oveq12  6084  cbvmpov  6158  ovmpog  6213  fvmpopr2d  6215  eqopi  6396  fmpoco  6442  supp0cosupp0fn  6497  imacosuppfn  6498  nnaordex  6791  map0g  6959  xpcomco  7114  xpmapenlem  7139  phplem3  7145  phplem4  7146  sbthlemi5  7268  addcmpblnq  7724  ltrnqg  7777  enq0ref  7790  addcmpblnq0  7800  distrlem4prl  7941  distrlem4pru  7942  recexgt0sr  8130  axcnre  8238  cnegexlem2  8492  cnegexlem3  8493  recexap  8971  xaddpnf2  10228  xaddmnf2  10230  rexadd  10233  xaddnemnf  10238  xaddnepnf  10239  xposdif  10263  frec2uzrand  10820  seqeq3  10867  seqf1oglem2  10935  seqf1og  10936  lsw1  11332  swrdccat  11485  ccats1pfxeqbi  11492  shftcan1  11577  remul2  11616  immul2  11623  fprodssdc  12335  ef0lem  12405  efieq1re  12517  dvdsnegb  12553  dvdscmul  12563  dvds2ln  12569  dvds2add  12570  dvds2sub  12571  gcdn0val  12716  rpmulgcd  12781  lcmval  12819  lcmn0val  12822  odzval  12998  pcmpt  13100  ballotfilemfp1  13209  grpsubval  13828  mulgnn0gzsum  13908  crngpropd  14317  opprringbg  14358  dvdsrtr  14381  isopn3  15149  dvexp  15735  dvexp2  15736  elply2  15759  lgsval3  16051  lgsdinn0  16081  incistruhgr  16245  clwwlkn1loopb  16575  clwwlkext2edg  16577  clwwlknonex2  16594  eupth2lem3lem3fi  16625  subctctexmid  16944