Theorem sylan9eq 2147

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452  ax-17 1471  ax-ext 2077

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

This theorem is referenced by:  sylan9req  2148  sylan9eqr  2149  difeq12  3128  uneq12  3164  ineq12  3211  ifeq12  3427  preq12  3541  prprc  3572  preq12b  3636  opeq12  3646  xpeq12  4486  nfimad  4816  coi2  4981  funimass1  5125  f1orescnv  5304  resdif  5310  oveq12  5699  cbvmpt2v  5766  ovmpt2g  5817  eqopi  5980  fmpt2co  6019  nnaordex  6326  map0g  6485  xpcomco  6622  xpmapenlem  6645  phplem3  6650  phplem4  6651  sbthlemi5  6750  addcmpblnq  7023  ltrnqg  7076  enq0ref  7089  addcmpblnq0  7099  distrlem4prl  7240  distrlem4pru  7241  recexgt0sr  7416  axcnre  7513  cnegexlem2  7755  cnegexlem3  7756  recexap  8219  xaddpnf2  9413  xaddmnf2  9415  rexadd  9418  xaddnemnf  9423  xaddnepnf  9424  xposdif  9448  frec2uzrand  9961  seqeq3  10005  shftcan1  10383  remul2  10422  immul2  10429  ef0lem  11099  efieq1re  11210  dvdsnegb  11240  dvdscmul  11250  dvds2ln  11256  dvds2add  11257  dvds2sub  11258  gcdn0val  11380  rpmulgcd  11442  lcmval  11472  lcmn0val  11475  isopn3  11977