Theorem syl6eqr 2190

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 2143	. 2 |- B = C
4	1, 3	syl6eq 2188	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 2121

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

This theorem is referenced by:  3eqtr4g  2197  rabxmdc  3394  relop  4689  csbcnvg  4723  dfiun3g  4796  dfiin3g  4797  resima2  4853  relcnvfld  5072  uniabio  5098  fntpg  5179  dffn5im  5467  dfimafn2  5471  fncnvima2  5541  fmptcof  5587  fcoconst  5591  fnasrng  5600  ffnov  5875  fnovim  5879  fnrnov  5916  foov  5917  funimassov  5920  ovelimab  5921  ofc12  6002  caofinvl  6004  dftpos3  6159  tfr0dm  6219  rdgisucinc  6282  oasuc  6360  ecinxp  6504  phplem1  6746  exmidpw  6802  unfiin  6814  fidcenumlemr  6843  0ct  6992  ctmlemr  6993  exmidaclem  7064  indpi  7150  nqnq0pi  7246  nq0m0r  7264  addnqpr1  7370  recexgt0sr  7581  suplocsrlempr  7615  recidpipr  7664  recidpirq  7666  axrnegex  7687  nntopi  7702  cnref1o  9440  fztp  9858  fseq1m1p1  9875  frecuzrdgrrn  10181  frecuzrdgsuc  10187  frecuzrdgsuctlem  10196  seq3val  10231  seqvalcd  10232  fser0const  10289  mulexpzap  10333  expaddzap  10337  bcp1m1  10511  cjexp  10665  rexuz3  10762  bdtri  11011  climconst  11059  sumfct  11143  zsumdc  11153  fsum3  11156  sum0  11157  fsumcnv  11206  mertenslem2  11305  ef0lem  11366  efzval  11389  efival  11439  sinbnd  11459  cosbnd  11460  eucalgval  11735  eucalginv  11737  eucalglt  11738  eucalgcvga  11739  eucalg  11740  sqpweven  11853  2sqpwodd  11854  dfphi2  11896  phimullem  11901  ennnfonelemhdmp1  11922  ennnfonelemkh  11925  ressid2  12018  ressval2  12019  topnvalg  12132  istps  12199  cldval  12268  ntrfval  12269  clsfval  12270  neifval  12309  restbasg  12337  tgrest  12338  txval  12424  upxp  12441  uptx  12443  txrest  12445  lmcn2  12449  cnmpt2t  12462  cnmpt2res  12466  imasnopn  12468  psmetxrge0  12501  xmetge0  12534  isxms  12620  isms  12622  bdxmet  12670  qtopbasss  12690  cnblcld  12704  negfcncf  12758  dvfvalap  12819  eldvap  12820  dvidlemap  12829  dvexp2  12845  dvrecap  12846  dveflem  12855  sin0pilem1  12862  ptolemy  12905  coskpi  12929  nninfsellemqall  13211