Theorem eqtr2d 2272

Description: An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)

Hypotheses

Ref	Expression
eqtr2d.1	|- ( ph -> A = B )
eqtr2d.2	|- ( ph -> B = C )

Assertion

Ref	Expression
eqtr2d	|- ( ph -> C = A )

Proof of Theorem eqtr2d

Step	Hyp	Ref	Expression
1		eqtr2d.1	. . 3 |- ( ph -> A = B )
2		eqtr2d.2	. . 3 |- ( ph -> B = C )
3	1, 2	eqtrd 2271	. 2 |- ( ph -> A = C )
4	3	eqcomd 2244	1 |- ( ph -> C = A )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtrrd  2276  3eqtr2rd  2278  ifandc  3681  ifordc  3682  onsucmin  4654  elxp4  5275  elxp5  5276  funopsn  5891  csbopeq1a  6422  ecinxp  6884  fundmen  7094  fidifsnen  7172  sbthlemi3  7276  ctm  7450  addpinq1  7832  1idsr  8136  prsradd  8154  cnegexlem3  8505  cnegex  8506  submul2  8728  mulsubfacd  8748  divadddivap  9060  infrenegsupex  10004  xadd4d  10298  fzval3  10633  fzoshftral  10668  ceiqm1l  10763  flqdiv  10773  flqmod  10790  intqfrac  10791  modqcyc2  10812  modqdi  10844  frecuzrdgtcl  10864  frecuzrdgfunlem  10871  seqf1oglem1  10971  seqf1oglem2  10972  seq3id2  10978  expnegzap  11025  binom2sub  11105  binom3  11109  resq01  11110  fihashssdif  11275  ccatw2s1p2  11430  ccats1pfxeq  11502  pfxccatin12lem2  11519  pfxccatin12  11521  swrdccat3b  11528  cats1fvnd  11553  reim  11633  mulreap  11645  addcj  11672  resqrexlemcalc1  11796  absimle  11867  infxrnegsupex  12048  clim2ser  12122  serf0  12137  summodclem3  12166  mptfzshft  12228  fsumrev  12229  fsum2mul  12239  isumsplit  12277  cvgratz  12318  mertenslemi1  12321  fprodrev  12405  ef4p  12480  tanval3ap  12500  efival  12518  sinmul  12530  divalglemnn  12704  dfgcd2  12810  lcmgcdlem  12874  lcm1  12878  nnmaxpwlemxy  12967  nnmaxpwlemparts  12971  eulerthlemth  13033  hashgcdeq  13041  powm2modprm  13054  pythagtriplem16  13081  pczpre  13099  pcqdiv  13109  pcadd  13142  pcfac  13152  4sqlem10  13189  4sqlem19  13211  ennnfonelemp1  13349  strslfvd  13446  xpsff1o  13723  gzsumsplit1r  13768  grpinvssd  13935  grpinvval2  13941  gzsumreidx  14225  gzsumshift  14233  gzsumgsum1  14237  gzsumgsum  14239  opprrngbg  14467  opprringbg  14469  ringinvdv  14536  lss1d  14804  znzrh2  15065  cnclima  15415  divcncfap  15806  dveflem  15918  plycjlemc  15952  tangtx  16031  abssinper  16039  reexplog  16065  rprelogbdiv  16154  birthdaylem2  16187  chtprm  16222  perfect1  16259  bcp1ctr  16267  bclbnd  16268  bposlem1  16272  lgsdirnn0  16332  lgsdinn0  16333  gausslemma2dlem1a  16343  gausslemma2dlem4  16349  gausslemma2dlem5a  16350  lgseisenlem2  16356  lgsquadlem1  16362  2sqlem2  16400  mul2sq  16401  ushgredgedgloop  16635  clwwlkext2edg  16829  pw1map  17191