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  4828  csbcnvg  4862  dfiun3g  4935  dfiin3g  4936  resima2  4993  relcnvfld  5216  uniabio  5242  fntpg  5330  dffn5im  5624  dfimafn2  5628  fncnvima2  5701  fmptcof  5747  fcoconst  5751  fnasrng  5760  funopsn  5762  ffnov  6049  fnovim  6054  fnrnov  6092  foov  6093  funimassov  6096  ovelimab  6097  ofc12  6182  caofinvl  6184  dftpos3  6348  tfr0dm  6408  rdgisucinc  6471  oasuc  6550  ecinxp  6697  phplem1  6949  exmidpw  7005  exmidpweq  7006  unfiin  7023  fidcenumlemr  7057  0ct  7209  ctmlemr  7210  exmidaclem  7320  indpi  7455  nqnq0pi  7551  nq0m0r  7569  addnqpr1  7675  recexgt0sr  7886  suplocsrlempr  7920  recidpipr  7969  recidpirq  7971  axrnegex  7992  nntopi  8007  cnref1o  9772  fztp  10200  fseq1m1p1  10217  fz0to4untppr  10246  frecuzrdgrrn  10553  frecuzrdgsuc  10559  frecuzrdgsuctlem  10568  seq3val  10605  seqvalcd  10606  fser0const  10680  mulexpzap  10724  expaddzap  10728  bcp1m1  10910  hash2en  10988  iswrdiz  11001  cjexp  11204  rexuz3  11301  bdtri  11551  climconst  11601  sumfct  11685  zsumdc  11695  fsum3  11698  sum0  11699  fsumcnv  11748  mertenslem2  11847  zproddc  11890  fprodseq  11894  prod0  11896  prod1dc  11897  prodfct  11898  fprodcnv  11936  ef0lem  11971  efzval  11994  efival  12043  sinbnd  12063  cosbnd  12064  eucalgval  12376  eucalginv  12378  eucalglt  12379  eucalgcvga  12380  eucalg  12381  sqpweven  12497  2sqpwodd  12498  dfphi2  12542  phimullem  12547  prmdiv  12557  odzval  12564  pcval  12619  pczpre  12620  pcrec  12631  4sqlem17  12730  ennnfonelemhdmp1  12780  ennnfonelemkh  12783  ressinbasd  12906  restid2  13080  topnvalg  13083  prdsval  13105  prdsbas3  13119  pwsval  13123  pwsbas  13124  pwselbasb  13125  pwsplusgval  13127  pwsmulrval  13128  imasival  13138  imasplusg  13140  qusval  13155  xpsval  13184  ismgm  13189  plusffvalg  13194  grpidvalg  13205  igsumvalx  13221  issgrp  13235  ismnddef  13250  pws0g  13283  ismhm  13293  isgrp  13338  grpn0  13367  grpinvfvalg  13374  grpsubfvalg  13377  pwsinvg  13444  mulgfvalg  13457  mulgval  13458  mulgnn0p1  13469  issubg  13509  isnsg  13538  eqgfval  13558  quseccl0g  13567  isghm  13579  conjsubg  13613  conjsubgen  13614  iscmn  13629  mgpvalg  13685  isrng  13696  issrg  13727  isring  13762  iscrng  13765  opprvalg  13831  dfrhm2  13916  isnzr  13943  islring  13954  issubrg  13983  rrgval  14024  isdomn  14031  islmod  14053  scaffvalg  14068  lsssetm  14118  lspfval  14150  2idlval  14264  2idlvalg  14265  mulgrhm2  14372  zlmval  14389  znval  14398  znzrhfo  14410  znle2  14414  psrval  14428  mplvalcoe  14452  istps  14504  cldval  14571  ntrfval  14572  clsfval  14573  neifval  14612  restbasg  14640  tgrest  14641  txval  14727  upxp  14744  uptx  14746  txrest  14748  lmcn2  14752  cnmpt2t  14765  cnmpt2res  14769  imasnopn  14771  psmetxrge0  14804  xmetge0  14837  isxms  14923  isms  14925  bdxmet  14973  qtopbasss  14993  cnblcld  15007  mpomulcn  15038  negfcncf  15078  dvfvalap  15153  eldvap  15154  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvexp2  15184  dvrecap  15185  dveflem  15198  plyconst  15217  plycolemc  15230  sin0pilem1  15253  ptolemy  15296  coskpi  15320  logbrec  15432  mpodvdsmulf1o  15462  fsumdvdsmul  15463  lgslem1  15477  lgsval  15481  lgsval4  15497  lgsfcl3  15498  lgsdilem  15504  lgsdir2lem4  15508  lgsdir2lem5  15509  gausslemma2dlem5  15543  lgsquadlem2  15555  iedgedgg  15655  nninfsellemqall  15956