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  7548  1idsr  7852  prsradd  7870  cnegexlem3  8220  cnegex  8221  submul2  8442  mulsubfacd  8462  divadddivap  8771  infrenegsupex  9685  xadd4d  9977  fzval3  10297  fzoshftral  10331  ceiqm1l  10420  flqdiv  10430  flqmod  10447  intqfrac  10448  modqcyc2  10469  modqdi  10501  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  seqf1oglem1  10628  seqf1oglem2  10629  seq3id2  10635  expnegzap  10682  binom2sub  10762  binom3  10766  fihashssdif  10927  reim  11034  mulreap  11046  addcj  11073  resqrexlemcalc1  11196  absimle  11266  infxrnegsupex  11445  clim2ser  11519  serf0  11534  summodclem3  11562  mptfzshft  11624  fsumrev  11625  fsum2mul  11635  isumsplit  11673  cvgratz  11714  mertenslemi1  11717  fprodrev  11801  ef4p  11876  tanval3ap  11896  efival  11914  sinmul  11926  divalglemnn  12100  dfgcd2  12206  lcmgcdlem  12270  lcm1  12274  oddpwdclemxy  12362  oddpwdclemdc  12366  eulerthlemth  12425  hashgcdeq  12433  powm2modprm  12446  pythagtriplem16  12473  pczpre  12491  pcqdiv  12501  pcadd  12534  pcfac  12544  4sqlem10  12581  4sqlem19  12603  ennnfonelemp1  12648  strslfvd  12745  xpsff1o  13051  gsumsplit1r  13100  grpinvssd  13279  grpinvval2  13285  gsumfzreidx  13543  opprrngbg  13710  opprringbg  13712  ringinvdv  13777  lss1d  14015  znzrh2  14278  cnclima  14543  divcncfap  14934  dveflem  15046  plycjlemc  15080  tangtx  15158  abssinper  15166  reexplog  15191  rprelogbdiv  15277  perfect1  15318  lgsdirnn0  15372  lgsdinn0  15373  gausslemma2dlem1a  15383  gausslemma2dlem4  15389  gausslemma2dlem5a  15390  lgseisenlem2  15396  lgsquadlem1  15402  2sqlem2  15440  mul2sq  15441