Theorem eqtr4di 2256

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

Syntax hints:   -> wi 4   = wceq 1373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198

This theorem is referenced by:  3eqtr4g  2263  rabxmdc  3492  relop  4829  csbcnvg  4863  dfiun3g  4936  dfiin3g  4937  resima2  4994  relcnvfld  5217  uniabio  5243  fntpg  5331  dffn5im  5626  dfimafn2  5630  fncnvima2  5703  fmptcof  5749  fcoconst  5753  fnasrng  5762  funopsn  5764  ffnov  6051  fnovim  6056  fnrnov  6094  foov  6095  funimassov  6098  ovelimab  6099  ofc12  6184  caofinvl  6186  dftpos3  6350  tfr0dm  6410  rdgisucinc  6473  oasuc  6552  ecinxp  6699  phplem1  6951  exmidpw  7007  exmidpweq  7008  unfiin  7025  fidcenumlemr  7059  0ct  7211  ctmlemr  7212  exmidaclem  7322  indpi  7457  nqnq0pi  7553  nq0m0r  7571  addnqpr1  7677  recexgt0sr  7888  suplocsrlempr  7922  recidpipr  7971  recidpirq  7973  axrnegex  7994  nntopi  8009  cnref1o  9774  fztp  10202  fseq1m1p1  10219  fz0to4untppr  10248  frecuzrdgrrn  10555  frecuzrdgsuc  10561  frecuzrdgsuctlem  10570  seq3val  10607  seqvalcd  10608  fser0const  10682  mulexpzap  10726  expaddzap  10730  bcp1m1  10912  hash2en  10990  iswrdiz  11003  cjexp  11237  rexuz3  11334  bdtri  11584  climconst  11634  sumfct  11718  zsumdc  11728  fsum3  11731  sum0  11732  fsumcnv  11781  mertenslem2  11880  zproddc  11923  fprodseq  11927  prod0  11929  prod1dc  11930  prodfct  11931  fprodcnv  11969  ef0lem  12004  efzval  12027  efival  12076  sinbnd  12096  cosbnd  12097  eucalgval  12409  eucalginv  12411  eucalglt  12412  eucalgcvga  12413  eucalg  12414  sqpweven  12530  2sqpwodd  12531  dfphi2  12575  phimullem  12580  prmdiv  12590  odzval  12597  pcval  12652  pczpre  12653  pcrec  12664  4sqlem17  12763  ennnfonelemhdmp1  12813  ennnfonelemkh  12816  ressinbasd  12939  restid2  13113  topnvalg  13116  prdsval  13138  prdsbas3  13152  pwsval  13156  pwsbas  13157  pwselbasb  13158  pwsplusgval  13160  pwsmulrval  13161  imasival  13171  imasplusg  13173  qusval  13188  xpsval  13217  ismgm  13222  plusffvalg  13227  grpidvalg  13238  igsumvalx  13254  issgrp  13268  ismnddef  13283  pws0g  13316  ismhm  13326  isgrp  13371  grpn0  13400  grpinvfvalg  13407  grpsubfvalg  13410  pwsinvg  13477  mulgfvalg  13490  mulgval  13491  mulgnn0p1  13502  issubg  13542  isnsg  13571  eqgfval  13591  quseccl0g  13600  isghm  13612  conjsubg  13646  conjsubgen  13647  iscmn  13662  mgpvalg  13718  isrng  13729  issrg  13760  isring  13795  iscrng  13798  opprvalg  13864  dfrhm2  13949  isnzr  13976  islring  13987  issubrg  14016  rrgval  14057  isdomn  14064  islmod  14086  scaffvalg  14101  lsssetm  14151  lspfval  14183  2idlval  14297  2idlvalg  14298  mulgrhm2  14405  zlmval  14422  znval  14431  znzrhfo  14443  znle2  14447  psrval  14461  mplvalcoe  14485  istps  14537  cldval  14604  ntrfval  14605  clsfval  14606  neifval  14645  restbasg  14673  tgrest  14674  txval  14760  upxp  14777  uptx  14779  txrest  14781  lmcn2  14785  cnmpt2t  14798  cnmpt2res  14802  imasnopn  14804  psmetxrge0  14837  xmetge0  14870  isxms  14956  isms  14958  bdxmet  15006  qtopbasss  15026  cnblcld  15040  mpomulcn  15071  negfcncf  15111  dvfvalap  15186  eldvap  15187  dvidlemap  15196  dvidrelem  15197  dvidsslem  15198  dvexp2  15217  dvrecap  15218  dveflem  15231  plyconst  15250  plycolemc  15263  sin0pilem1  15286  ptolemy  15329  coskpi  15353  logbrec  15465  mpodvdsmulf1o  15495  fsumdvdsmul  15496  lgslem1  15510  lgsval  15514  lgsval4  15530  lgsfcl3  15531  lgsdilem  15537  lgsdir2lem4  15541  lgsdir2lem5  15542  gausslemma2dlem5  15576  lgsquadlem2  15588  iedgedgg  15688  nninfsellemqall  15989