Theorem eqtr2d 2265

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

Syntax hints:   -> wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224

This theorem is referenced by:  3eqtrrd  2269  3eqtr2rd  2271  ifandc  3646  ifordc  3647  onsucmin  4605  elxp4  5224  elxp5  5225  funopsn  5830  csbopeq1a  6351  ecinxp  6779  fundmen  6981  fidifsnen  7057  sbthlemi3  7158  ctm  7308  addpinq1  7684  1idsr  7988  prsradd  8006  cnegexlem3  8356  cnegex  8357  submul2  8578  mulsubfacd  8598  divadddivap  8907  infrenegsupex  9828  xadd4d  10120  fzval3  10450  fzoshftral  10485  ceiqm1l  10574  flqdiv  10584  flqmod  10601  intqfrac  10602  modqcyc2  10623  modqdi  10655  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  seqf1oglem1  10782  seqf1oglem2  10783  seq3id2  10789  expnegzap  10836  binom2sub  10916  binom3  10920  fihashssdif  11083  ccatw2s1p2  11227  ccats1pfxeq  11299  pfxccatin12lem2  11316  pfxccatin12  11318  swrdccat3b  11325  cats1fvnd  11350  reim  11430  mulreap  11442  addcj  11469  resqrexlemcalc1  11592  absimle  11662  infxrnegsupex  11841  clim2ser  11915  serf0  11930  summodclem3  11959  mptfzshft  12021  fsumrev  12022  fsum2mul  12032  isumsplit  12070  cvgratz  12111  mertenslemi1  12114  fprodrev  12198  ef4p  12273  tanval3ap  12293  efival  12311  sinmul  12323  divalglemnn  12497  dfgcd2  12603  lcmgcdlem  12667  lcm1  12671  oddpwdclemxy  12759  oddpwdclemdc  12763  eulerthlemth  12822  hashgcdeq  12830  powm2modprm  12843  pythagtriplem16  12870  pczpre  12888  pcqdiv  12898  pcadd  12931  pcfac  12941  4sqlem10  12978  4sqlem19  13000  ennnfonelemp1  13045  strslfvd  13142  xpsff1o  13450  gsumsplit1r  13499  grpinvssd  13678  grpinvval2  13684  gsumfzreidx  13942  opprrngbg  14110  opprringbg  14112  ringinvdv  14178  lss1d  14416  znzrh2  14679  cnclima  14966  divcncfap  15357  dveflem  15469  plycjlemc  15503  tangtx  15581  abssinper  15589  reexplog  15614  rprelogbdiv  15700  perfect1  15741  lgsdirnn0  15795  lgsdinn0  15796  gausslemma2dlem1a  15806  gausslemma2dlem4  15812  gausslemma2dlem5a  15813  lgseisenlem2  15819  lgsquadlem1  15825  2sqlem2  15863  mul2sq  15864  ushgredgedgloop  16098  clwwlkext2edg  16292  pw1map  16647  gsumgfsum1  16733  gsumgfsum  16736