Theorem eqtr4di 2221

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

Syntax hints:   -> wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  3eqtr4g  2228  rabxmdc  3446  relop  4761  csbcnvg  4795  dfiun3g  4868  dfiin3g  4869  resima2  4925  relcnvfld  5144  uniabio  5170  fntpg  5254  dffn5im  5542  dfimafn2  5546  fncnvima2  5617  fmptcof  5663  fcoconst  5667  fnasrng  5676  ffnov  5957  fnovim  5961  fnrnov  5998  foov  5999  funimassov  6002  ovelimab  6003  ofc12  6081  caofinvl  6083  dftpos3  6241  tfr0dm  6301  rdgisucinc  6364  oasuc  6443  ecinxp  6588  phplem1  6830  exmidpw  6886  exmidpweq  6887  unfiin  6903  fidcenumlemr  6932  0ct  7084  ctmlemr  7085  exmidaclem  7185  indpi  7304  nqnq0pi  7400  nq0m0r  7418  addnqpr1  7524  recexgt0sr  7735  suplocsrlempr  7769  recidpipr  7818  recidpirq  7820  axrnegex  7841  nntopi  7856  cnref1o  9609  fztp  10034  fseq1m1p1  10051  fz0to4untppr  10080  frecuzrdgrrn  10364  frecuzrdgsuc  10370  frecuzrdgsuctlem  10379  seq3val  10414  seqvalcd  10415  fser0const  10472  mulexpzap  10516  expaddzap  10520  bcp1m1  10699  cjexp  10857  rexuz3  10954  bdtri  11203  climconst  11253  sumfct  11337  zsumdc  11347  fsum3  11350  sum0  11351  fsumcnv  11400  mertenslem2  11499  zproddc  11542  fprodseq  11546  prod0  11548  prod1dc  11549  prodfct  11550  fprodcnv  11588  ef0lem  11623  efzval  11646  efival  11695  sinbnd  11715  cosbnd  11716  eucalgval  12008  eucalginv  12010  eucalglt  12011  eucalgcvga  12012  eucalg  12013  sqpweven  12129  2sqpwodd  12130  dfphi2  12174  phimullem  12179  prmdiv  12189  odzval  12195  pcval  12250  pczpre  12251  pcrec  12262  ennnfonelemhdmp1  12364  ennnfonelemkh  12367  ressid2  12477  ressval2  12478  topnvalg  12591  ismgm  12611  plusffvalg  12616  grpidvalg  12627  issgrp  12644  ismnddef  12654  ismhm  12685  isgrp  12714  grpn0  12738  grpinvfvalg  12745  grpsubfvalg  12748  istps  12824  cldval  12893  ntrfval  12894  clsfval  12895  neifval  12934  restbasg  12962  tgrest  12963  txval  13049  upxp  13066  uptx  13068  txrest  13070  lmcn2  13074  cnmpt2t  13087  cnmpt2res  13091  imasnopn  13093  psmetxrge0  13126  xmetge0  13159  isxms  13245  isms  13247  bdxmet  13295  qtopbasss  13315  cnblcld  13329  negfcncf  13383  dvfvalap  13444  eldvap  13445  dvidlemap  13454  dvexp2  13470  dvrecap  13471  dveflem  13481  sin0pilem1  13496  ptolemy  13539  coskpi  13563  logbrec  13672  lgslem1  13695  lgsval  13699  lgsval4  13715  lgsfcl3  13716  lgsdilem  13722  lgsdir2lem4  13726  lgsdir2lem5  13727  nninfsellemqall  14048