Theorem syl5eq 2133

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl5eq.1	|- A = B
syl5eq.2	|- ( ph -> B = C )

Assertion

Ref	Expression
syl5eq	|- ( ph -> A = C )

Proof of Theorem syl5eq

Step	Hyp	Ref	Expression
1		syl5eq.1	. . 3 |- A = B
2	1	a1i 9	. 2 |- ( ph -> A = B )
3		syl5eq.2	. 2 |- ( ph -> B = C )
4	2, 3	eqtrd 2121	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1290

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 1382  ax-gen 1384  ax-4 1446  ax-17 1465  ax-ext 2071

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

This theorem is referenced by:  syl5req  2134  syl5eqr  2135  3eqtr3a  2145  3eqtr4g  2146  csbtt  2944  csbvarg  2959  csbie2g  2979  rabbi2dva  3209  csbprc  3332  disjssun  3350  disjpr2  3510  prprc2  3555  difprsn2  3583  opprc  3649  intsng  3728  riinm  3808  iinxsng  3809  rintm  3827  sucprc  4248  unisucg  4250  xpriindim  4587  relop  4599  dmxpm  4669  riinint  4707  resabs1  4755  resabs2  4756  resima2  4759  xpssres  4760  resopab2  4772  imasng  4810  ndmima  4822  xpdisj1  4868  xpdisj2  4869  djudisj  4871  resdisj  4872  rnxpm  4873  xpima1  4890  xpima2m  4891  dmsnsnsng  4921  rnsnopg  4922  rnpropg  4923  mptiniseg  4938  dfco2a  4944  relcoi1  4975  unixpm  4979  iotaval  5004  funtp  5080  fnun  5133  fnresdisj  5137  fnima  5145  fnimaeq0  5148  fcoi1  5204  f1orescnv  5282  foun  5285  resdif  5288  tz6.12-2  5309  fveu  5310  tz6.12-1  5344  fvun2  5384  fvopab3ig  5391  f1oresrab  5477  dfmptg  5490  ressnop0  5492  fvunsng  5505  fnsnsplitss  5510  fsnunfv  5512  fvpr1  5515  fvpr2  5516  fvpr1g  5517  fvpr2g  5518  fvtp1g  5519  fvtp2g  5520  fvtp3g  5521  fvtp2  5523  fvtp3  5524  f1oiso2  5620  riotaund  5656  ovprc  5698  resoprab2  5756  fnoprabg  5760  ovidig  5776  ovigg  5779  ov6g  5796  ovconst2  5810  offval2  5884  ot1stg  5937  ot2ndg  5938  ot3rdgg  5939  fmpt2co  5995  algrflemg  6009  tpostpos2  6044  rdgisuc1  6163  frec0g  6176  frecsuclem  6185  frecrdg  6187  oasuc  6239  oa1suc  6242  omsuc  6247  nnm1  6297  nnm2  6298  dfec2  6309  errn  6328  ixpsnval  6472  ixpintm  6496  mapen  6616  xpmapenlem  6619  phplem2  6623  undifdc  6688  fisseneq  6696  ssfirab  6697  eqinfti  6769  infvalti  6771  infsnti  6779  casef  6833  caseinl  6836  djudom  6837  exmidfodomrlemim  6888  1qec  7008  mulidnq  7009  addpinq1  7084  0idsr  7374  1idsr  7375  caucvgsrlemoffres  7406  caucvgsr  7408  mulresr  7436  pitonnlem2  7445  ax1rid  7473  axcnre  7477  negid  7790  subneg  7792  negneg  7793  dfinfre  8478  2times  8605  infrenegsupex  9143  rexneg  9353  fseq1p1m1  9569  fzosplitprm1  9706  intfracq  9788  frec2uz0d  9867  frec2uzrdg  9877  frecuzrdg0  9881  frecuzrdgg  9884  frecuzrdg0t  9890  iseqval  9932  iseqvalt  9934  seq3val  9935  iseqf1olemjpcl  9985  iseqf1olemqpcl  9986  iseqf1olemfvp  9987  seq3f1olemqsum  9990  sqval  10074  iexpcyc  10120  binom3  10132  faclbnd  10210  faclbnd2  10211  bcn1  10227  hashinfom  10247  hashennn  10249  hashxp  10295  shftlem  10311  shftuz  10312  shftidt  10328  reim0  10356  remullem  10366  resqrexlemf1  10502  resqrexlemcalc3  10510  absexpzap  10574  absimle  10578  amgm2  10612  minmax  10722  isummo  10834  fisum  10839  sumsnf  10864  sumsns  10870  isumclim3  10878  isumge0  10885  fsump1i  10888  fsum2dlemstep  10889  fisumcom2  10893  fsumshftm  10900  fsumconst  10909  fsumiun  10932  hashrabrex  10936  hashuni  10937  binom11  10941  isumsplit  10946  geo2sum  10969  mertensabs  10992  efgt1p2  11046  efgt1p  11047  resinval  11067  recosval  11068  cosadd  11089  ef01bndlem  11108  eirraplem  11125  ialgr0  11365  algrp1  11367  eucalg  11380  phiprmpw  11537  phiprm  11538  ndxid  11579  setsfun0  11591  setsresg  11593  setscom  11595  strslfv2d  11597  ressid2  11614  ressval2  11615  tgidm  11835  divccncfap  11919  ex-ceil  11926  qdencn  12187