Theorem sylan9eq 2287

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 2252	. 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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  sylan9req  2288  sylan9eqr  2289  difeq12  3336  uneq12  3372  ineq12  3421  ifeq12  3643  preq12  3775  prprc  3807  preq12b  3879  opeq12  3890  xpeq12  4773  nfimad  5115  coi2  5284  funimass1  5438  f1orescnv  5635  resdif  5641  oveq12  6067  cbvmpov  6141  ovmpog  6196  fvmpopr2d  6198  eqopi  6379  fmpoco  6425  supp0cosupp0fn  6480  imacosuppfn  6481  nnaordex  6774  map0g  6935  xpcomco  7090  xpmapenlem  7115  phplem3  7121  phplem4  7122  sbthlemi5  7244  addcmpblnq  7698  ltrnqg  7751  enq0ref  7764  addcmpblnq0  7774  distrlem4prl  7915  distrlem4pru  7916  recexgt0sr  8104  axcnre  8212  cnegexlem2  8465  cnegexlem3  8466  recexap  8944  xaddpnf2  10199  xaddmnf2  10201  rexadd  10204  xaddnemnf  10209  xaddnepnf  10210  xposdif  10234  frec2uzrand  10791  seqeq3  10838  seqf1oglem2  10906  seqf1og  10907  lsw1  11299  swrdccat  11452  ccats1pfxeqbi  11459  shftcan1  11544  remul2  11583  immul2  11590  fprodssdc  12301  ef0lem  12371  efieq1re  12483  dvdsnegb  12519  dvdscmul  12529  dvds2ln  12535  dvds2add  12536  dvds2sub  12537  gcdn0val  12682  rpmulgcd  12747  lcmval  12785  lcmn0val  12788  odzval  12964  pcmpt  13066  ballotfilemfp1  13175  grpsubval  13801  mulgnn0gsum  13881  crngpropd  14282  opprringbg  14323  dvdsrtr  14346  isopn3  15116  dvexp  15702  dvexp2  15703  elply2  15726  lgsval3  16017  lgsdinn0  16047  incistruhgr  16211  clwwlkn1loopb  16541  clwwlkext2edg  16543  clwwlknonex2  16560  eupth2lem3lem3fi  16591  subctctexmid  16900