Theorem eqtr4di 2215

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

Hypotheses

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

Assertion

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

Proof of Theorem eqtr4di

Step	Hyp	Ref	Expression
1		eqtr4di.1	. 2 |- ( ph -> A = B )
2		eqtr4di.2	. . 3 |- C = B
3	2	eqcomi 2168	. 2 |- B = C
4	1, 3	eqtrdi 2213	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1342

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 1434  ax-gen 1436  ax-4 1497  ax-17 1513  ax-ext 2146

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

This theorem is referenced by:  3eqtr4g  2222  rabxmdc  3435  relop  4748  csbcnvg  4782  dfiun3g  4855  dfiin3g  4856  resima2  4912  relcnvfld  5131  uniabio  5157  fntpg  5238  dffn5im  5526  dfimafn2  5530  fncnvima2  5600  fmptcof  5646  fcoconst  5650  fnasrng  5659  ffnov  5937  fnovim  5941  fnrnov  5978  foov  5979  funimassov  5982  ovelimab  5983  ofc12  6064  caofinvl  6066  dftpos3  6221  tfr0dm  6281  rdgisucinc  6344  oasuc  6423  ecinxp  6567  phplem1  6809  exmidpw  6865  exmidpweq  6866  unfiin  6882  fidcenumlemr  6911  0ct  7063  ctmlemr  7064  exmidaclem  7155  indpi  7274  nqnq0pi  7370  nq0m0r  7388  addnqpr1  7494  recexgt0sr  7705  suplocsrlempr  7739  recidpipr  7788  recidpirq  7790  axrnegex  7811  nntopi  7826  cnref1o  9579  fztp  10003  fseq1m1p1  10020  fz0to4untppr  10049  frecuzrdgrrn  10333  frecuzrdgsuc  10339  frecuzrdgsuctlem  10348  seq3val  10383  seqvalcd  10384  fser0const  10441  mulexpzap  10485  expaddzap  10489  bcp1m1  10667  cjexp  10821  rexuz3  10918  bdtri  11167  climconst  11217  sumfct  11301  zsumdc  11311  fsum3  11314  sum0  11315  fsumcnv  11364  mertenslem2  11463  zproddc  11506  fprodseq  11510  prod0  11512  prod1dc  11513  prodfct  11514  fprodcnv  11552  ef0lem  11587  efzval  11610  efival  11659  sinbnd  11679  cosbnd  11680  eucalgval  11965  eucalginv  11967  eucalglt  11968  eucalgcvga  11969  eucalg  11970  sqpweven  12084  2sqpwodd  12085  dfphi2  12129  phimullem  12134  prmdiv  12144  odzval  12150  pcval  12205  pczpre  12206  pcrec  12217  ennnfonelemhdmp1  12279  ennnfonelemkh  12282  ressid2  12390  ressval2  12391  topnvalg  12504  istps  12571  cldval  12640  ntrfval  12641  clsfval  12642  neifval  12681  restbasg  12709  tgrest  12710  txval  12796  upxp  12813  uptx  12815  txrest  12817  lmcn2  12821  cnmpt2t  12834  cnmpt2res  12838  imasnopn  12840  psmetxrge0  12873  xmetge0  12906  isxms  12992  isms  12994  bdxmet  13042  qtopbasss  13062  cnblcld  13076  negfcncf  13130  dvfvalap  13191  eldvap  13192  dvidlemap  13201  dvexp2  13217  dvrecap  13218  dveflem  13228  sin0pilem1  13243  ptolemy  13286  coskpi  13310  logbrec  13419  nninfsellemqall  13729