Theorem syl6eqr 2188

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

Hypotheses

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

Assertion

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

Proof of Theorem syl6eqr

Step	Hyp	Ref	Expression
1		syl6eqr.1	. 2 |- ( ph -> A = B )
2		syl6eqr.2	. . 3 |- C = B
3	2	eqcomi 2141	. 2 |- B = C
4	1, 3	syl6eq 2186	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

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

This theorem is referenced by:  3eqtr4g  2195  rabxmdc  3389  relop  4684  csbcnvg  4718  dfiun3g  4791  dfiin3g  4792  resima2  4848  relcnvfld  5067  uniabio  5093  fntpg  5174  dffn5im  5460  dfimafn2  5464  fncnvima2  5534  fmptcof  5580  fcoconst  5584  fnasrng  5593  ffnov  5868  fnovim  5872  fnrnov  5909  foov  5910  funimassov  5913  ovelimab  5914  ofc12  5995  caofinvl  5997  dftpos3  6152  tfr0dm  6212  rdgisucinc  6275  oasuc  6353  ecinxp  6497  phplem1  6739  exmidpw  6795  unfiin  6807  fidcenumlemr  6836  0ct  6985  ctmlemr  6986  exmidaclem  7057  indpi  7143  nqnq0pi  7239  nq0m0r  7257  addnqpr1  7363  recexgt0sr  7574  suplocsrlempr  7608  recidpipr  7657  recidpirq  7659  axrnegex  7680  nntopi  7695  cnref1o  9433  fztp  9851  fseq1m1p1  9868  frecuzrdgrrn  10174  frecuzrdgsuc  10180  frecuzrdgsuctlem  10189  seq3val  10224  seqvalcd  10225  fser0const  10282  mulexpzap  10326  expaddzap  10330  bcp1m1  10504  cjexp  10658  rexuz3  10755  bdtri  11004  climconst  11052  sumfct  11136  zsumdc  11146  fsum3  11149  sum0  11150  fsumcnv  11199  mertenslem2  11298  ef0lem  11355  efzval  11378  efival  11428  sinbnd  11448  cosbnd  11449  eucalgval  11724  eucalginv  11726  eucalglt  11727  eucalgcvga  11728  eucalg  11729  sqpweven  11842  2sqpwodd  11843  dfphi2  11885  phimullem  11890  ennnfonelemhdmp1  11911  ennnfonelemkh  11914  ressid2  12007  ressval2  12008  topnvalg  12121  istps  12188  cldval  12257  ntrfval  12258  clsfval  12259  neifval  12298  restbasg  12326  tgrest  12327  txval  12413  upxp  12430  uptx  12432  txrest  12434  lmcn2  12438  cnmpt2t  12451  cnmpt2res  12455  imasnopn  12457  psmetxrge0  12490  xmetge0  12523  isxms  12609  isms  12611  bdxmet  12659  qtopbasss  12679  cnblcld  12693  negfcncf  12747  dvfvalap  12808  eldvap  12809  dvidlemap  12818  dvexp2  12834  dvrecap  12835  dveflem  12844  sin0pilem1  12851  ptolemy  12894  coskpi  12918  nninfsellemqall  13200