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  3478  relop  4812  csbcnvg  4846  dfiun3g  4919  dfiin3g  4920  resima2  4976  relcnvfld  5199  uniabio  5225  fntpg  5310  dffn5im  5602  dfimafn2  5606  fncnvima2  5679  fmptcof  5725  fcoconst  5729  fnasrng  5738  ffnov  6022  fnovim  6027  fnrnov  6064  foov  6065  funimassov  6068  ovelimab  6069  ofc12  6153  caofinvl  6155  dftpos3  6315  tfr0dm  6375  rdgisucinc  6438  oasuc  6517  ecinxp  6664  phplem1  6908  exmidpw  6964  exmidpweq  6965  unfiin  6982  fidcenumlemr  7014  0ct  7166  ctmlemr  7167  exmidaclem  7268  indpi  7402  nqnq0pi  7498  nq0m0r  7516  addnqpr1  7622  recexgt0sr  7833  suplocsrlempr  7867  recidpipr  7916  recidpirq  7918  axrnegex  7939  nntopi  7954  cnref1o  9716  fztp  10144  fseq1m1p1  10161  fz0to4untppr  10190  frecuzrdgrrn  10479  frecuzrdgsuc  10485  frecuzrdgsuctlem  10494  seq3val  10531  seqvalcd  10532  fser0const  10606  mulexpzap  10650  expaddzap  10654  bcp1m1  10836  iswrdiz  10921  cjexp  11037  rexuz3  11134  bdtri  11383  climconst  11433  sumfct  11517  zsumdc  11527  fsum3  11530  sum0  11531  fsumcnv  11580  mertenslem2  11679  zproddc  11722  fprodseq  11726  prod0  11728  prod1dc  11729  prodfct  11730  fprodcnv  11768  ef0lem  11803  efzval  11826  efival  11875  sinbnd  11895  cosbnd  11896  eucalgval  12192  eucalginv  12194  eucalglt  12195  eucalgcvga  12196  eucalg  12197  sqpweven  12313  2sqpwodd  12314  dfphi2  12358  phimullem  12363  prmdiv  12373  odzval  12379  pcval  12434  pczpre  12435  pcrec  12446  4sqlem17  12545  ennnfonelemhdmp1  12566  ennnfonelemkh  12569  ressinbasd  12692  restid2  12859  topnvalg  12862  imasival  12889  imasplusg  12891  qusval  12906  xpsval  12935  ismgm  12940  plusffvalg  12945  grpidvalg  12956  igsumvalx  12972  issgrp  12986  ismnddef  12999  ismhm  13033  isgrp  13078  grpn0  13107  grpinvfvalg  13114  grpsubfvalg  13117  mulgfvalg  13191  mulgval  13192  mulgnn0p1  13203  issubg  13243  isnsg  13272  eqgfval  13292  quseccl0g  13301  isghm  13313  conjsubg  13347  conjsubgen  13348  iscmn  13363  mgpvalg  13419  isrng  13430  issrg  13461  isring  13496  iscrng  13499  opprvalg  13565  dfrhm2  13650  isnzr  13677  islring  13688  issubrg  13717  rrgval  13758  isdomn  13765  islmod  13787  scaffvalg  13802  lsssetm  13852  lspfval  13884  2idlval  13998  2idlvalg  13999  mulgrhm2  14098  zlmval  14115  znval  14124  znzrhfo  14136  znle2  14140  psrval  14152  istps  14200  cldval  14267  ntrfval  14268  clsfval  14269  neifval  14308  restbasg  14336  tgrest  14337  txval  14423  upxp  14440  uptx  14442  txrest  14444  lmcn2  14448  cnmpt2t  14461  cnmpt2res  14465  imasnopn  14467  psmetxrge0  14500  xmetge0  14533  isxms  14619  isms  14621  bdxmet  14669  qtopbasss  14689  cnblcld  14703  negfcncf  14760  dvfvalap  14835  eldvap  14836  dvidlemap  14845  dvexp2  14861  dvrecap  14862  dveflem  14872  plyconst  14891  sin0pilem1  14916  ptolemy  14959  coskpi  14983  logbrec  15092  lgslem1  15116  lgsval  15120  lgsval4  15136  lgsfcl3  15137  lgsdilem  15143  lgsdir2lem4  15147  lgsdir2lem5  15148  gausslemma2dlem5  15182  nninfsellemqall  15505