Theorem eqtr2d 2239

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

Syntax hints:   -> wi 4   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  3eqtrrd  2243  3eqtr2rd  2245  ifandc  3610  ifordc  3611  onsucmin  4555  elxp4  5170  elxp5  5171  funopsn  5762  csbopeq1a  6274  ecinxp  6697  fundmen  6898  fidifsnen  6967  sbthlemi3  7061  ctm  7211  addpinq1  7577  1idsr  7881  prsradd  7899  cnegexlem3  8249  cnegex  8250  submul2  8471  mulsubfacd  8491  divadddivap  8800  infrenegsupex  9715  xadd4d  10007  fzval3  10333  fzoshftral  10367  ceiqm1l  10456  flqdiv  10466  flqmod  10483  intqfrac  10484  modqcyc2  10505  modqdi  10537  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  seqf1oglem1  10664  seqf1oglem2  10665  seq3id2  10671  expnegzap  10718  binom2sub  10798  binom3  10802  fihashssdif  10963  ccatw2s1p2  11097  reim  11163  mulreap  11175  addcj  11202  resqrexlemcalc1  11325  absimle  11395  infxrnegsupex  11574  clim2ser  11648  serf0  11663  summodclem3  11691  mptfzshft  11753  fsumrev  11754  fsum2mul  11764  isumsplit  11802  cvgratz  11843  mertenslemi1  11846  fprodrev  11930  ef4p  12005  tanval3ap  12025  efival  12043  sinmul  12055  divalglemnn  12229  dfgcd2  12335  lcmgcdlem  12399  lcm1  12403  oddpwdclemxy  12491  oddpwdclemdc  12495  eulerthlemth  12554  hashgcdeq  12562  powm2modprm  12575  pythagtriplem16  12602  pczpre  12620  pcqdiv  12630  pcadd  12663  pcfac  12673  4sqlem10  12710  4sqlem19  12732  ennnfonelemp1  12777  strslfvd  12874  xpsff1o  13181  gsumsplit1r  13230  grpinvssd  13409  grpinvval2  13415  gsumfzreidx  13673  opprrngbg  13840  opprringbg  13842  ringinvdv  13907  lss1d  14145  znzrh2  14408  cnclima  14695  divcncfap  15086  dveflem  15198  plycjlemc  15232  tangtx  15310  abssinper  15318  reexplog  15343  rprelogbdiv  15429  perfect1  15470  lgsdirnn0  15524  lgsdinn0  15525  gausslemma2dlem1a  15535  gausslemma2dlem4  15541  gausslemma2dlem5a  15542  lgseisenlem2  15548  lgsquadlem1  15554  2sqlem2  15592  mul2sq  15593