Theorem eqtr4di 2258

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 2211	. 2 |- B = C
4	1, 3	eqtrdi 2256	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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  3eqtr4g  2265  rabxmdc  3500  relop  4846  csbcnvg  4880  dfiun3g  4954  dfiin3g  4955  resima2  5012  relcnvfld  5235  uniabio  5261  fntpg  5349  dffn5im  5647  dfimafn2  5651  fncnvima2  5724  fmptcof  5770  fcoconst  5774  fnasrng  5783  funopsn  5785  ffnov  6072  fnovim  6077  fnrnov  6115  foov  6116  funimassov  6119  ovelimab  6120  ofc12  6205  caofinvl  6207  dftpos3  6371  tfr0dm  6431  rdgisucinc  6494  oasuc  6573  ecinxp  6720  phplem1  6974  exmidpw  7031  exmidpweq  7032  unfiin  7049  fidcenumlemr  7083  0ct  7235  ctmlemr  7236  exmidaclem  7351  pw1m  7370  indpi  7490  nqnq0pi  7586  nq0m0r  7604  addnqpr1  7710  recexgt0sr  7921  suplocsrlempr  7955  recidpipr  8004  recidpirq  8006  axrnegex  8027  nntopi  8042  cnref1o  9807  fztp  10235  fseq1m1p1  10252  fz0to4untppr  10281  frecuzrdgrrn  10590  frecuzrdgsuc  10596  frecuzrdgsuctlem  10605  seq3val  10642  seqvalcd  10643  fser0const  10717  mulexpzap  10761  expaddzap  10765  bcp1m1  10947  hash2en  11025  iswrdiz  11038  pfxccatin12lem2c  11221  cjexp  11319  rexuz3  11416  bdtri  11666  climconst  11716  sumfct  11800  zsumdc  11810  fsum3  11813  sum0  11814  fsumcnv  11863  mertenslem2  11962  zproddc  12005  fprodseq  12009  prod0  12011  prod1dc  12012  prodfct  12013  fprodcnv  12051  ef0lem  12086  efzval  12109  efival  12158  sinbnd  12178  cosbnd  12179  eucalgval  12491  eucalginv  12493  eucalglt  12494  eucalgcvga  12495  eucalg  12496  sqpweven  12612  2sqpwodd  12613  dfphi2  12657  phimullem  12662  prmdiv  12672  odzval  12679  pcval  12734  pczpre  12735  pcrec  12746  4sqlem17  12845  ennnfonelemhdmp1  12895  ennnfonelemkh  12898  ressinbasd  13021  restid2  13195  topnvalg  13198  prdsval  13220  prdsbas3  13234  pwsval  13238  pwsbas  13239  pwselbasb  13240  pwsplusgval  13242  pwsmulrval  13243  imasival  13253  imasplusg  13255  qusval  13270  xpsval  13299  ismgm  13304  plusffvalg  13309  grpidvalg  13320  igsumvalx  13336  issgrp  13350  ismnddef  13365  pws0g  13398  ismhm  13408  isgrp  13453  grpn0  13482  grpinvfvalg  13489  grpsubfvalg  13492  pwsinvg  13559  mulgfvalg  13572  mulgval  13573  mulgnn0p1  13584  issubg  13624  isnsg  13653  eqgfval  13673  quseccl0g  13682  isghm  13694  conjsubg  13728  conjsubgen  13729  iscmn  13744  mgpvalg  13800  isrng  13811  issrg  13842  isring  13877  iscrng  13880  opprvalg  13946  dfrhm2  14031  isnzr  14058  islring  14069  issubrg  14098  rrgval  14139  isdomn  14146  islmod  14168  scaffvalg  14183  lsssetm  14233  lspfval  14265  2idlval  14379  2idlvalg  14380  mulgrhm2  14487  zlmval  14504  znval  14513  znzrhfo  14525  znle2  14529  psrval  14543  mplvalcoe  14567  istps  14619  cldval  14686  ntrfval  14687  clsfval  14688  neifval  14727  restbasg  14755  tgrest  14756  txval  14842  upxp  14859  uptx  14861  txrest  14863  lmcn2  14867  cnmpt2t  14880  cnmpt2res  14884  imasnopn  14886  psmetxrge0  14919  xmetge0  14952  isxms  15038  isms  15040  bdxmet  15088  qtopbasss  15108  cnblcld  15122  mpomulcn  15153  negfcncf  15193  dvfvalap  15268  eldvap  15269  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dvexp2  15299  dvrecap  15300  dveflem  15313  plyconst  15332  plycolemc  15345  sin0pilem1  15368  ptolemy  15411  coskpi  15435  logbrec  15547  mpodvdsmulf1o  15577  fsumdvdsmul  15578  lgslem1  15592  lgsval  15596  lgsval4  15612  lgsfcl3  15613  lgsdilem  15619  lgsdir2lem4  15623  lgsdir2lem5  15624  gausslemma2dlem5  15658  lgsquadlem2  15670  iedgedgg  15772  isuhgrm  15782  isushgrm  15783  isupgren  15806  isumgren  15816  nninfsellemqall  16154