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  5609  dfimafn2  5613  fncnvima2  5686  fmptcof  5732  fcoconst  5736  fnasrng  5745  ffnov  6030  fnovim  6035  fnrnov  6073  foov  6074  funimassov  6077  ovelimab  6078  ofc12  6163  caofinvl  6165  dftpos3  6329  tfr0dm  6389  rdgisucinc  6452  oasuc  6531  ecinxp  6678  phplem1  6922  exmidpw  6978  exmidpweq  6979  unfiin  6996  fidcenumlemr  7030  0ct  7182  ctmlemr  7183  exmidaclem  7291  indpi  7426  nqnq0pi  7522  nq0m0r  7540  addnqpr1  7646  recexgt0sr  7857  suplocsrlempr  7891  recidpipr  7940  recidpirq  7942  axrnegex  7963  nntopi  7978  cnref1o  9742  fztp  10170  fseq1m1p1  10187  fz0to4untppr  10216  frecuzrdgrrn  10517  frecuzrdgsuc  10523  frecuzrdgsuctlem  10532  seq3val  10569  seqvalcd  10570  fser0const  10644  mulexpzap  10688  expaddzap  10692  bcp1m1  10874  iswrdiz  10959  cjexp  11075  rexuz3  11172  bdtri  11422  climconst  11472  sumfct  11556  zsumdc  11566  fsum3  11569  sum0  11570  fsumcnv  11619  mertenslem2  11718  zproddc  11761  fprodseq  11765  prod0  11767  prod1dc  11768  prodfct  11769  fprodcnv  11807  ef0lem  11842  efzval  11865  efival  11914  sinbnd  11934  cosbnd  11935  eucalgval  12247  eucalginv  12249  eucalglt  12250  eucalgcvga  12251  eucalg  12252  sqpweven  12368  2sqpwodd  12369  dfphi2  12413  phimullem  12418  prmdiv  12428  odzval  12435  pcval  12490  pczpre  12491  pcrec  12502  4sqlem17  12601  ennnfonelemhdmp1  12651  ennnfonelemkh  12654  ressinbasd  12777  restid2  12950  topnvalg  12953  prdsval  12975  prdsbas3  12989  pwsval  12993  pwsbas  12994  pwselbasb  12995  pwsplusgval  12997  pwsmulrval  12998  imasival  13008  imasplusg  13010  qusval  13025  xpsval  13054  ismgm  13059  plusffvalg  13064  grpidvalg  13075  igsumvalx  13091  issgrp  13105  ismnddef  13120  pws0g  13153  ismhm  13163  isgrp  13208  grpn0  13237  grpinvfvalg  13244  grpsubfvalg  13247  pwsinvg  13314  mulgfvalg  13327  mulgval  13328  mulgnn0p1  13339  issubg  13379  isnsg  13408  eqgfval  13428  quseccl0g  13437  isghm  13449  conjsubg  13483  conjsubgen  13484  iscmn  13499  mgpvalg  13555  isrng  13566  issrg  13597  isring  13632  iscrng  13635  opprvalg  13701  dfrhm2  13786  isnzr  13813  islring  13824  issubrg  13853  rrgval  13894  isdomn  13901  islmod  13923  scaffvalg  13938  lsssetm  13988  lspfval  14020  2idlval  14134  2idlvalg  14135  mulgrhm2  14242  zlmval  14259  znval  14268  znzrhfo  14280  znle2  14284  psrval  14296  istps  14352  cldval  14419  ntrfval  14420  clsfval  14421  neifval  14460  restbasg  14488  tgrest  14489  txval  14575  upxp  14592  uptx  14594  txrest  14596  lmcn2  14600  cnmpt2t  14613  cnmpt2res  14617  imasnopn  14619  psmetxrge0  14652  xmetge0  14685  isxms  14771  isms  14773  bdxmet  14821  qtopbasss  14841  cnblcld  14855  mpomulcn  14886  negfcncf  14926  dvfvalap  15001  eldvap  15002  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvexp2  15032  dvrecap  15033  dveflem  15046  plyconst  15065  plycolemc  15078  sin0pilem1  15101  ptolemy  15144  coskpi  15168  logbrec  15280  mpodvdsmulf1o  15310  fsumdvdsmul  15311  lgslem1  15325  lgsval  15329  lgsval4  15345  lgsfcl3  15346  lgsdilem  15352  lgsdir2lem4  15356  lgsdir2lem5  15357  gausslemma2dlem5  15391  lgsquadlem2  15403  nninfsellemqall  15746