Theorem eqtr2d 2230

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 2229	. 2 |- ( ph -> A = C )
4	3	eqcomd 2202	1 |- ( ph -> C = A )

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:  3eqtrrd  2234  3eqtr2rd  2236  ifandc  3599  ifordc  3600  onsucmin  4543  elxp4  5157  elxp5  5158  csbopeq1a  6246  ecinxp  6669  fundmen  6865  fidifsnen  6931  sbthlemi3  7025  ctm  7175  addpinq1  7531  1idsr  7835  prsradd  7853  cnegexlem3  8203  cnegex  8204  submul2  8425  mulsubfacd  8445  divadddivap  8754  infrenegsupex  9668  xadd4d  9960  fzval3  10280  fzoshftral  10314  ceiqm1l  10403  flqdiv  10413  flqmod  10430  intqfrac  10431  modqcyc2  10452  modqdi  10484  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  seqf1oglem1  10611  seqf1oglem2  10612  seq3id2  10618  expnegzap  10665  binom2sub  10745  binom3  10749  fihashssdif  10910  reim  11017  mulreap  11029  addcj  11056  resqrexlemcalc1  11179  absimle  11249  infxrnegsupex  11428  clim2ser  11502  serf0  11517  summodclem3  11545  mptfzshft  11607  fsumrev  11608  fsum2mul  11618  isumsplit  11656  cvgratz  11697  mertenslemi1  11700  fprodrev  11784  ef4p  11859  tanval3ap  11879  efival  11897  sinmul  11909  divalglemnn  12083  dfgcd2  12181  lcmgcdlem  12245  lcm1  12249  oddpwdclemxy  12337  oddpwdclemdc  12341  eulerthlemth  12400  hashgcdeq  12408  powm2modprm  12421  pythagtriplem16  12448  pczpre  12466  pcqdiv  12476  pcadd  12509  pcfac  12519  4sqlem10  12556  4sqlem19  12578  ennnfonelemp1  12623  strslfvd  12720  xpsff1o  12992  gsumsplit1r  13041  grpinvssd  13209  grpinvval2  13215  gsumfzreidx  13467  opprrngbg  13634  opprringbg  13636  ringinvdv  13701  lss1d  13939  znzrh2  14202  cnclima  14459  divcncfap  14850  dveflem  14962  plycjlemc  14996  tangtx  15074  abssinper  15082  reexplog  15107  rprelogbdiv  15193  perfect1  15234  lgsdirnn0  15288  lgsdinn0  15289  gausslemma2dlem1a  15299  gausslemma2dlem4  15305  gausslemma2dlem5a  15306  lgseisenlem2  15312  lgsquadlem1  15318  2sqlem2  15356  mul2sq  15357