Theorem eqtr4di 2217

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 2169	. 2 |- B = C
4	1, 3	eqtrdi 2215	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  3eqtr4g  2224  rabxmdc  3440  relop  4754  csbcnvg  4788  dfiun3g  4861  dfiin3g  4862  resima2  4918  relcnvfld  5137  uniabio  5163  fntpg  5244  dffn5im  5532  dfimafn2  5536  fncnvima2  5606  fmptcof  5652  fcoconst  5656  fnasrng  5665  ffnov  5946  fnovim  5950  fnrnov  5987  foov  5988  funimassov  5991  ovelimab  5992  ofc12  6070  caofinvl  6072  dftpos3  6230  tfr0dm  6290  rdgisucinc  6353  oasuc  6432  ecinxp  6576  phplem1  6818  exmidpw  6874  exmidpweq  6875  unfiin  6891  fidcenumlemr  6920  0ct  7072  ctmlemr  7073  exmidaclem  7164  indpi  7283  nqnq0pi  7379  nq0m0r  7397  addnqpr1  7503  recexgt0sr  7714  suplocsrlempr  7748  recidpipr  7797  recidpirq  7799  axrnegex  7820  nntopi  7835  cnref1o  9588  fztp  10013  fseq1m1p1  10030  fz0to4untppr  10059  frecuzrdgrrn  10343  frecuzrdgsuc  10349  frecuzrdgsuctlem  10358  seq3val  10393  seqvalcd  10394  fser0const  10451  mulexpzap  10495  expaddzap  10499  bcp1m1  10678  cjexp  10835  rexuz3  10932  bdtri  11181  climconst  11231  sumfct  11315  zsumdc  11325  fsum3  11328  sum0  11329  fsumcnv  11378  mertenslem2  11477  zproddc  11520  fprodseq  11524  prod0  11526  prod1dc  11527  prodfct  11528  fprodcnv  11566  ef0lem  11601  efzval  11624  efival  11673  sinbnd  11693  cosbnd  11694  eucalgval  11986  eucalginv  11988  eucalglt  11989  eucalgcvga  11990  eucalg  11991  sqpweven  12107  2sqpwodd  12108  dfphi2  12152  phimullem  12157  prmdiv  12167  odzval  12173  pcval  12228  pczpre  12229  pcrec  12240  ennnfonelemhdmp1  12342  ennnfonelemkh  12345  ressid2  12454  ressval2  12455  topnvalg  12568  ismgm  12588  plusffvalg  12593  grpidvalg  12604  istps  12670  cldval  12739  ntrfval  12740  clsfval  12741  neifval  12780  restbasg  12808  tgrest  12809  txval  12895  upxp  12912  uptx  12914  txrest  12916  lmcn2  12920  cnmpt2t  12933  cnmpt2res  12937  imasnopn  12939  psmetxrge0  12972  xmetge0  13005  isxms  13091  isms  13093  bdxmet  13141  qtopbasss  13161  cnblcld  13175  negfcncf  13229  dvfvalap  13290  eldvap  13291  dvidlemap  13300  dvexp2  13316  dvrecap  13317  dveflem  13327  sin0pilem1  13342  ptolemy  13385  coskpi  13409  logbrec  13518  lgslem1  13541  lgsval  13545  lgsval4  13561  lgsfcl3  13562  lgsdilem  13568  lgsdir2lem4  13572  lgsdir2lem5  13573  nninfsellemqall  13895