Theorem sylan9eq 2282

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 2247	. 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 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  sylan9req  2283  sylan9eqr  2284  difeq12  3317  uneq12  3353  ineq12  3400  ifeq12  3619  preq12  3745  prprc  3777  preq12b  3848  opeq12  3859  xpeq12  4738  nfimad  5077  coi2  5245  funimass1  5398  f1orescnv  5588  resdif  5594  oveq12  6010  cbvmpov  6084  ovmpog  6139  fvmpopr2d  6141  eqopi  6318  fmpoco  6362  nnaordex  6674  map0g  6835  xpcomco  6985  xpmapenlem  7010  phplem3  7015  phplem4  7016  sbthlemi5  7128  addcmpblnq  7554  ltrnqg  7607  enq0ref  7620  addcmpblnq0  7630  distrlem4prl  7771  distrlem4pru  7772  recexgt0sr  7960  axcnre  8068  cnegexlem2  8322  cnegexlem3  8323  recexap  8800  xaddpnf2  10043  xaddmnf2  10045  rexadd  10048  xaddnemnf  10053  xaddnepnf  10054  xposdif  10078  frec2uzrand  10627  seqeq3  10674  seqf1oglem2  10742  seqf1og  10743  lsw1  11121  swrdccat  11267  ccats1pfxeqbi  11274  shftcan1  11345  remul2  11384  immul2  11391  fprodssdc  12101  ef0lem  12171  efieq1re  12283  dvdsnegb  12319  dvdscmul  12329  dvds2ln  12335  dvds2add  12336  dvds2sub  12337  gcdn0val  12482  rpmulgcd  12547  lcmval  12585  lcmn0val  12588  odzval  12764  pcmpt  12866  grpsubval  13579  mulgnn0gsum  13665  crngpropd  14002  opprringbg  14043  dvdsrtr  14065  isopn3  14799  dvexp  15385  dvexp2  15386  elply2  15409  lgsval3  15697  lgsdinn0  15727  incistruhgr  15890  subctctexmid  16366