Theorem eqtr2d 2263

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtrrd  2267  3eqtr2rd  2269  ifandc  3643  ifordc  3644  onsucmin  4599  elxp4  5216  elxp5  5217  funopsn  5819  csbopeq1a  6340  ecinxp  6765  fundmen  6967  fidifsnen  7040  sbthlemi3  7137  ctm  7287  addpinq1  7662  1idsr  7966  prsradd  7984  cnegexlem3  8334  cnegex  8335  submul2  8556  mulsubfacd  8576  divadddivap  8885  infrenegsupex  9801  xadd4d  10093  fzval3  10422  fzoshftral  10456  ceiqm1l  10545  flqdiv  10555  flqmod  10572  intqfrac  10573  modqcyc2  10594  modqdi  10626  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  seqf1oglem1  10753  seqf1oglem2  10754  seq3id2  10760  expnegzap  10807  binom2sub  10887  binom3  10891  fihashssdif  11053  ccatw2s1p2  11191  ccats1pfxeq  11261  pfxccatin12lem2  11278  pfxccatin12  11280  swrdccat3b  11287  cats1fvnd  11312  reim  11378  mulreap  11390  addcj  11417  resqrexlemcalc1  11540  absimle  11610  infxrnegsupex  11789  clim2ser  11863  serf0  11878  summodclem3  11906  mptfzshft  11968  fsumrev  11969  fsum2mul  11979  isumsplit  12017  cvgratz  12058  mertenslemi1  12061  fprodrev  12145  ef4p  12220  tanval3ap  12240  efival  12258  sinmul  12270  divalglemnn  12444  dfgcd2  12550  lcmgcdlem  12614  lcm1  12618  oddpwdclemxy  12706  oddpwdclemdc  12710  eulerthlemth  12769  hashgcdeq  12777  powm2modprm  12790  pythagtriplem16  12817  pczpre  12835  pcqdiv  12845  pcadd  12878  pcfac  12888  4sqlem10  12925  4sqlem19  12947  ennnfonelemp1  12992  strslfvd  13089  xpsff1o  13397  gsumsplit1r  13446  grpinvssd  13625  grpinvval2  13631  gsumfzreidx  13889  opprrngbg  14056  opprringbg  14058  ringinvdv  14124  lss1d  14362  znzrh2  14625  cnclima  14912  divcncfap  15303  dveflem  15415  plycjlemc  15449  tangtx  15527  abssinper  15535  reexplog  15560  rprelogbdiv  15646  perfect1  15687  lgsdirnn0  15741  lgsdinn0  15742  gausslemma2dlem1a  15752  gausslemma2dlem4  15758  gausslemma2dlem5a  15759  lgseisenlem2  15765  lgsquadlem1  15771  2sqlem2  15809  mul2sq  15810  ushgredgedgloop  16041  pw1map  16420