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  3600  ifordc  3601  onsucmin  4544  elxp4  5158  elxp5  5159  csbopeq1a  6255  ecinxp  6678  fundmen  6874  fidifsnen  6940  sbthlemi3  7034  ctm  7184  addpinq1  7550  1idsr  7854  prsradd  7872  cnegexlem3  8222  cnegex  8223  submul2  8444  mulsubfacd  8464  divadddivap  8773  infrenegsupex  9687  xadd4d  9979  fzval3  10299  fzoshftral  10333  ceiqm1l  10422  flqdiv  10432  flqmod  10449  intqfrac  10450  modqcyc2  10471  modqdi  10503  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  seqf1oglem1  10630  seqf1oglem2  10631  seq3id2  10637  expnegzap  10684  binom2sub  10764  binom3  10768  fihashssdif  10929  reim  11036  mulreap  11048  addcj  11075  resqrexlemcalc1  11198  absimle  11268  infxrnegsupex  11447  clim2ser  11521  serf0  11536  summodclem3  11564  mptfzshft  11626  fsumrev  11627  fsum2mul  11637  isumsplit  11675  cvgratz  11716  mertenslemi1  11719  fprodrev  11803  ef4p  11878  tanval3ap  11898  efival  11916  sinmul  11928  divalglemnn  12102  dfgcd2  12208  lcmgcdlem  12272  lcm1  12276  oddpwdclemxy  12364  oddpwdclemdc  12368  eulerthlemth  12427  hashgcdeq  12435  powm2modprm  12448  pythagtriplem16  12475  pczpre  12493  pcqdiv  12503  pcadd  12536  pcfac  12546  4sqlem10  12583  4sqlem19  12605  ennnfonelemp1  12650  strslfvd  12747  xpsff1o  13053  gsumsplit1r  13102  grpinvssd  13281  grpinvval2  13287  gsumfzreidx  13545  opprrngbg  13712  opprringbg  13714  ringinvdv  13779  lss1d  14017  znzrh2  14280  cnclima  14567  divcncfap  14958  dveflem  15070  plycjlemc  15104  tangtx  15182  abssinper  15190  reexplog  15215  rprelogbdiv  15301  perfect1  15342  lgsdirnn0  15396  lgsdinn0  15397  gausslemma2dlem1a  15407  gausslemma2dlem4  15413  gausslemma2dlem5a  15414  lgseisenlem2  15420  lgsquadlem1  15426  2sqlem2  15464  mul2sq  15465