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  7449  addpinq1  7831  1idsr  8135  prsradd  8153  cnegexlem3  8504  cnegex  8505  submul2  8727  mulsubfacd  8747  divadddivap  9059  infrenegsupex  10003  xadd4d  10297  fzval3  10632  fzoshftral  10667  ceiqm1l  10761  flqdiv  10771  flqmod  10788  intqfrac  10789  modqcyc2  10810  modqdi  10842  frecuzrdgtcl  10862  frecuzrdgfunlem  10869  seqf1oglem1  10969  seqf1oglem2  10970  seq3id2  10976  expnegzap  11023  binom2sub  11103  binom3  11107  resq01  11108  fihashssdif  11273  ccatw2s1p2  11428  ccats1pfxeq  11500  pfxccatin12lem2  11517  pfxccatin12  11519  swrdccat3b  11526  cats1fvnd  11551  reim  11631  mulreap  11643  addcj  11670  resqrexlemcalc1  11794  absimle  11865  infxrnegsupex  12045  clim2ser  12119  serf0  12134  summodclem3  12163  mptfzshft  12225  fsumrev  12226  fsum2mul  12236  isumsplit  12274  cvgratz  12315  mertenslemi1  12318  fprodrev  12402  ef4p  12477  tanval3ap  12497  efival  12515  sinmul  12527  divalglemnn  12701  dfgcd2  12807  lcmgcdlem  12871  lcm1  12875  nnmaxpwlemxy  12964  nnmaxpwlemparts  12968  eulerthlemth  13030  hashgcdeq  13038  powm2modprm  13051  pythagtriplem16  13078  pczpre  13096  pcqdiv  13106  pcadd  13139  pcfac  13149  4sqlem10  13186  4sqlem19  13208  ennnfonelemp1  13346  strslfvd  13443  xpsff1o  13719  gzsumsplit1r  13764  grpinvssd  13931  grpinvval2  13937  gzsumreidx  14190  gzsumshift  14198  gzsumgsum1  14202  gzsumgsum  14204  opprrngbg  14432  opprringbg  14434  ringinvdv  14501  lss1d  14769  znzrh2  15030  cnclima  15373  divcncfap  15764  dveflem  15876  plycjlemc  15910  tangtx  15989  abssinper  15997  reexplog  16023  rprelogbdiv  16112  birthdaylem2  16145  perfect1  16196  bcp1ctr  16204  bclbnd  16205  bposlem1  16209  lgsdirnn0  16264  lgsdinn0  16265  gausslemma2dlem1a  16275  gausslemma2dlem4  16281  gausslemma2dlem5a  16282  lgseisenlem2  16288  lgsquadlem1  16294  2sqlem2  16332  mul2sq  16333  ushgredgedgloop  16567  clwwlkext2edg  16761  pw1map  17123