Theorem sylan9eq 2260

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 2225	. 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 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  sylan9req  2261  sylan9eqr  2262  difeq12  3294  uneq12  3330  ineq12  3377  ifeq12  3596  preq12  3722  prprc  3753  preq12b  3824  opeq12  3835  xpeq12  4712  nfimad  5050  coi2  5218  funimass1  5370  f1orescnv  5560  resdif  5566  oveq12  5976  cbvmpov  6048  ovmpog  6103  fvmpopr2d  6105  eqopi  6281  fmpoco  6325  nnaordex  6637  map0g  6798  xpcomco  6946  xpmapenlem  6971  phplem3  6976  phplem4  6977  sbthlemi5  7089  addcmpblnq  7515  ltrnqg  7568  enq0ref  7581  addcmpblnq0  7591  distrlem4prl  7732  distrlem4pru  7733  recexgt0sr  7921  axcnre  8029  cnegexlem2  8283  cnegexlem3  8284  recexap  8761  xaddpnf2  10004  xaddmnf2  10006  rexadd  10009  xaddnemnf  10014  xaddnepnf  10015  xposdif  10039  frec2uzrand  10587  seqeq3  10634  seqf1oglem2  10702  seqf1og  10703  lsw1  11080  swrdccat  11226  ccats1pfxeqbi  11233  shftcan1  11260  remul2  11299  immul2  11306  fprodssdc  12016  ef0lem  12086  efieq1re  12198  dvdsnegb  12234  dvdscmul  12244  dvds2ln  12250  dvds2add  12251  dvds2sub  12252  gcdn0val  12397  rpmulgcd  12462  lcmval  12500  lcmn0val  12503  odzval  12679  pcmpt  12781  grpsubval  13493  mulgnn0gsum  13579  crngpropd  13916  opprringbg  13957  dvdsrtr  13978  isopn3  14712  dvexp  15298  dvexp2  15299  elply2  15322  lgsval3  15610  lgsdinn0  15640  incistruhgr  15801  subctctexmid  16139