Theorem eqtr4di 2244

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 2197	. 2 |- B = C
4	1, 3	eqtrdi 2242	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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  3eqtr4g  2251  rabxmdc  3479  relop  4813  csbcnvg  4847  dfiun3g  4920  dfiin3g  4921  resima2  4977  relcnvfld  5200  uniabio  5226  fntpg  5311  dffn5im  5603  dfimafn2  5607  fncnvima2  5680  fmptcof  5726  fcoconst  5730  fnasrng  5739  ffnov  6023  fnovim  6028  fnrnov  6066  foov  6067  funimassov  6070  ovelimab  6071  ofc12  6155  caofinvl  6157  dftpos3  6317  tfr0dm  6377  rdgisucinc  6440  oasuc  6519  ecinxp  6666  phplem1  6910  exmidpw  6966  exmidpweq  6967  unfiin  6984  fidcenumlemr  7016  0ct  7168  ctmlemr  7169  exmidaclem  7270  indpi  7404  nqnq0pi  7500  nq0m0r  7518  addnqpr1  7624  recexgt0sr  7835  suplocsrlempr  7869  recidpipr  7918  recidpirq  7920  axrnegex  7941  nntopi  7956  cnref1o  9719  fztp  10147  fseq1m1p1  10164  fz0to4untppr  10193  frecuzrdgrrn  10482  frecuzrdgsuc  10488  frecuzrdgsuctlem  10497  seq3val  10534  seqvalcd  10535  fser0const  10609  mulexpzap  10653  expaddzap  10657  bcp1m1  10839  iswrdiz  10924  cjexp  11040  rexuz3  11137  bdtri  11386  climconst  11436  sumfct  11520  zsumdc  11530  fsum3  11533  sum0  11534  fsumcnv  11583  mertenslem2  11682  zproddc  11725  fprodseq  11729  prod0  11731  prod1dc  11732  prodfct  11733  fprodcnv  11771  ef0lem  11806  efzval  11829  efival  11878  sinbnd  11898  cosbnd  11899  eucalgval  12195  eucalginv  12197  eucalglt  12198  eucalgcvga  12199  eucalg  12200  sqpweven  12316  2sqpwodd  12317  dfphi2  12361  phimullem  12366  prmdiv  12376  odzval  12382  pcval  12437  pczpre  12438  pcrec  12449  4sqlem17  12548  ennnfonelemhdmp1  12569  ennnfonelemkh  12572  ressinbasd  12695  restid2  12862  topnvalg  12865  imasival  12892  imasplusg  12894  qusval  12909  xpsval  12938  ismgm  12943  plusffvalg  12948  grpidvalg  12959  igsumvalx  12975  issgrp  12989  ismnddef  13002  ismhm  13036  isgrp  13081  grpn0  13110  grpinvfvalg  13117  grpsubfvalg  13120  mulgfvalg  13194  mulgval  13195  mulgnn0p1  13206  issubg  13246  isnsg  13275  eqgfval  13295  quseccl0g  13304  isghm  13316  conjsubg  13350  conjsubgen  13351  iscmn  13366  mgpvalg  13422  isrng  13433  issrg  13464  isring  13499  iscrng  13502  opprvalg  13568  dfrhm2  13653  isnzr  13680  islring  13691  issubrg  13720  rrgval  13761  isdomn  13768  islmod  13790  scaffvalg  13805  lsssetm  13855  lspfval  13887  2idlval  14001  2idlvalg  14002  mulgrhm2  14109  zlmval  14126  znval  14135  znzrhfo  14147  znle2  14151  psrval  14163  istps  14211  cldval  14278  ntrfval  14279  clsfval  14280  neifval  14319  restbasg  14347  tgrest  14348  txval  14434  upxp  14451  uptx  14453  txrest  14455  lmcn2  14459  cnmpt2t  14472  cnmpt2res  14476  imasnopn  14478  psmetxrge0  14511  xmetge0  14544  isxms  14630  isms  14632  bdxmet  14680  qtopbasss  14700  cnblcld  14714  mpomulcn  14745  negfcncf  14785  dvfvalap  14860  eldvap  14861  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvexp2  14891  dvrecap  14892  dveflem  14905  plyconst  14924  plycolemc  14936  sin0pilem1  14957  ptolemy  15000  coskpi  15024  logbrec  15133  lgslem1  15157  lgsval  15161  lgsval4  15177  lgsfcl3  15178  lgsdilem  15184  lgsdir2lem4  15188  lgsdir2lem5  15189  gausslemma2dlem5  15223  lgsquadlem2  15235  nninfsellemqall  15575