Theorem eqtr4di 2247

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

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtr4g  2254  rabxmdc  3483  relop  4817  csbcnvg  4851  dfiun3g  4924  dfiin3g  4925  resima2  4981  relcnvfld  5204  uniabio  5230  fntpg  5315  dffn5im  5607  dfimafn2  5611  fncnvima2  5684  fmptcof  5730  fcoconst  5734  fnasrng  5743  ffnov  6028  fnovim  6033  fnrnov  6071  foov  6072  funimassov  6075  ovelimab  6076  ofc12  6160  caofinvl  6162  dftpos3  6322  tfr0dm  6382  rdgisucinc  6445  oasuc  6524  ecinxp  6671  phplem1  6915  exmidpw  6971  exmidpweq  6972  unfiin  6989  fidcenumlemr  7023  0ct  7175  ctmlemr  7176  exmidaclem  7278  indpi  7412  nqnq0pi  7508  nq0m0r  7526  addnqpr1  7632  recexgt0sr  7843  suplocsrlempr  7877  recidpipr  7926  recidpirq  7928  axrnegex  7949  nntopi  7964  cnref1o  9728  fztp  10156  fseq1m1p1  10173  fz0to4untppr  10202  frecuzrdgrrn  10503  frecuzrdgsuc  10509  frecuzrdgsuctlem  10518  seq3val  10555  seqvalcd  10556  fser0const  10630  mulexpzap  10674  expaddzap  10678  bcp1m1  10860  iswrdiz  10945  cjexp  11061  rexuz3  11158  bdtri  11408  climconst  11458  sumfct  11542  zsumdc  11552  fsum3  11555  sum0  11556  fsumcnv  11605  mertenslem2  11704  zproddc  11747  fprodseq  11751  prod0  11753  prod1dc  11754  prodfct  11755  fprodcnv  11793  ef0lem  11828  efzval  11851  efival  11900  sinbnd  11920  cosbnd  11921  eucalgval  12233  eucalginv  12235  eucalglt  12236  eucalgcvga  12237  eucalg  12238  sqpweven  12354  2sqpwodd  12355  dfphi2  12399  phimullem  12404  prmdiv  12414  odzval  12421  pcval  12476  pczpre  12477  pcrec  12488  4sqlem17  12587  ennnfonelemhdmp1  12637  ennnfonelemkh  12640  ressinbasd  12763  restid2  12936  topnvalg  12939  prdsval  12961  imasival  12975  imasplusg  12977  qusval  12992  xpsval  13021  ismgm  13026  plusffvalg  13031  grpidvalg  13042  igsumvalx  13058  issgrp  13072  ismnddef  13085  ismhm  13119  isgrp  13164  grpn0  13193  grpinvfvalg  13200  grpsubfvalg  13203  mulgfvalg  13277  mulgval  13278  mulgnn0p1  13289  issubg  13329  isnsg  13358  eqgfval  13378  quseccl0g  13387  isghm  13399  conjsubg  13433  conjsubgen  13434  iscmn  13449  mgpvalg  13505  isrng  13516  issrg  13547  isring  13582  iscrng  13585  opprvalg  13651  dfrhm2  13736  isnzr  13763  islring  13774  issubrg  13803  rrgval  13844  isdomn  13851  islmod  13873  scaffvalg  13888  lsssetm  13938  lspfval  13970  2idlval  14084  2idlvalg  14085  mulgrhm2  14192  zlmval  14209  znval  14218  znzrhfo  14230  znle2  14234  psrval  14246  istps  14294  cldval  14361  ntrfval  14362  clsfval  14363  neifval  14402  restbasg  14430  tgrest  14431  txval  14517  upxp  14534  uptx  14536  txrest  14538  lmcn2  14542  cnmpt2t  14555  cnmpt2res  14559  imasnopn  14561  psmetxrge0  14594  xmetge0  14627  isxms  14713  isms  14715  bdxmet  14763  qtopbasss  14783  cnblcld  14797  mpomulcn  14828  negfcncf  14868  dvfvalap  14943  eldvap  14944  dvidlemap  14953  dvidrelem  14954  dvidsslem  14955  dvexp2  14974  dvrecap  14975  dveflem  14988  plyconst  15007  plycolemc  15020  sin0pilem1  15043  ptolemy  15086  coskpi  15110  logbrec  15222  mpodvdsmulf1o  15252  fsumdvdsmul  15253  lgslem1  15267  lgsval  15271  lgsval4  15287  lgsfcl3  15288  lgsdilem  15294  lgsdir2lem4  15298  lgsdir2lem5  15299  gausslemma2dlem5  15333  lgsquadlem2  15345  nninfsellemqall  15686