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  5590  resdif  5596  oveq12  6016  cbvmpov  6090  ovmpog  6145  fvmpopr2d  6147  eqopi  6324  fmpoco  6368  nnaordex  6682  map0g  6843  xpcomco  6993  xpmapenlem  7018  phplem3  7023  phplem4  7024  sbthlemi5  7139  addcmpblnq  7565  ltrnqg  7618  enq0ref  7631  addcmpblnq0  7641  distrlem4prl  7782  distrlem4pru  7783  recexgt0sr  7971  axcnre  8079  cnegexlem2  8333  cnegexlem3  8334  recexap  8811  xaddpnf2  10055  xaddmnf2  10057  rexadd  10060  xaddnemnf  10065  xaddnepnf  10066  xposdif  10090  frec2uzrand  10639  seqeq3  10686  seqf1oglem2  10754  seqf1og  10755  lsw1  11134  swrdccat  11283  ccats1pfxeqbi  11290  shftcan1  11361  remul2  11400  immul2  11407  fprodssdc  12117  ef0lem  12187  efieq1re  12299  dvdsnegb  12335  dvdscmul  12345  dvds2ln  12351  dvds2add  12352  dvds2sub  12353  gcdn0val  12498  rpmulgcd  12563  lcmval  12601  lcmn0val  12604  odzval  12780  pcmpt  12882  grpsubval  13595  mulgnn0gsum  13681  crngpropd  14018  opprringbg  14059  dvdsrtr  14081  isopn3  14815  dvexp  15401  dvexp2  15402  elply2  15425  lgsval3  15713  lgsdinn0  15743  incistruhgr  15906  clwwlkn1loopb  16162  clwwlkext2edg  16164  subctctexmid  16453