Theorem sylan9eq 2219

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 2183	. 2 |- ( ( A = B /\ B = C ) -> A = C )
4	1, 2, 3	syl2an 287	1 |- ( ( ph /\ ps ) -> A = C )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  sylan9req  2220  sylan9eqr  2221  difeq12  3235  uneq12  3271  ineq12  3318  ifeq12  3536  preq12  3655  prprc  3686  preq12b  3750  opeq12  3760  xpeq12  4623  nfimad  4955  coi2  5120  funimass1  5265  f1orescnv  5448  resdif  5454  oveq12  5851  cbvmpov  5922  ovmpog  5976  eqopi  6140  fmpoco  6184  nnaordex  6495  map0g  6654  xpcomco  6792  xpmapenlem  6815  phplem3  6820  phplem4  6821  sbthlemi5  6926  addcmpblnq  7308  ltrnqg  7361  enq0ref  7374  addcmpblnq0  7384  distrlem4prl  7525  distrlem4pru  7526  recexgt0sr  7714  axcnre  7822  cnegexlem2  8074  cnegexlem3  8075  recexap  8550  xaddpnf2  9783  xaddmnf2  9785  rexadd  9788  xaddnemnf  9793  xaddnepnf  9794  xposdif  9818  frec2uzrand  10340  seqeq3  10385  shftcan1  10776  remul2  10815  immul2  10822  fprodssdc  11531  ef0lem  11601  efieq1re  11712  dvdsnegb  11748  dvdscmul  11758  dvds2ln  11764  dvds2add  11765  dvds2sub  11766  gcdn0val  11894  rpmulgcd  11959  lcmval  11995  lcmn0val  11998  odzval  12173  pcmpt  12273  isopn3  12765  dvexp  13315  dvexp2  13316  lgsval3  13559  lgsdinn0  13589  subctctexmid  13881