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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  3eqtrrd  2269  3eqtr2rd  2271  ifandc  3650  ifordc  3651  onsucmin  4611  elxp4  5231  elxp5  5232  funopsn  5838  csbopeq1a  6360  ecinxp  6822  fundmen  7024  fidifsnen  7100  sbthlemi3  7201  ctm  7351  addpinq1  7727  1idsr  8031  prsradd  8049  cnegexlem3  8398  cnegex  8399  submul2  8620  mulsubfacd  8640  divadddivap  8949  infrenegsupex  9872  xadd4d  10164  fzval3  10495  fzoshftral  10530  ceiqm1l  10619  flqdiv  10629  flqmod  10646  intqfrac  10647  modqcyc2  10668  modqdi  10700  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  seqf1oglem1  10827  seqf1oglem2  10828  seq3id2  10834  expnegzap  10881  binom2sub  10961  binom3  10965  fihashssdif  11128  ccatw2s1p2  11272  ccats1pfxeq  11344  pfxccatin12lem2  11361  pfxccatin12  11363  swrdccat3b  11370  cats1fvnd  11395  reim  11475  mulreap  11487  addcj  11514  resqrexlemcalc1  11637  absimle  11707  infxrnegsupex  11886  clim2ser  11960  serf0  11975  summodclem3  12004  mptfzshft  12066  fsumrev  12067  fsum2mul  12077  isumsplit  12115  cvgratz  12156  mertenslemi1  12159  fprodrev  12243  ef4p  12318  tanval3ap  12338  efival  12356  sinmul  12368  divalglemnn  12542  dfgcd2  12648  lcmgcdlem  12712  lcm1  12716  oddpwdclemxy  12804  oddpwdclemdc  12808  eulerthlemth  12867  hashgcdeq  12875  powm2modprm  12888  pythagtriplem16  12915  pczpre  12933  pcqdiv  12943  pcadd  12976  pcfac  12986  4sqlem10  13023  4sqlem19  13045  ennnfonelemp1  13090  strslfvd  13187  xpsff1o  13495  gsumsplit1r  13544  grpinvssd  13723  grpinvval2  13729  gsumfzreidx  13987  opprrngbg  14155  opprringbg  14157  ringinvdv  14223  lss1d  14462  znzrh2  14725  cnclima  15017  divcncfap  15408  dveflem  15520  plycjlemc  15554  tangtx  15632  abssinper  15640  reexplog  15665  rprelogbdiv  15751  perfect1  15795  lgsdirnn0  15849  lgsdinn0  15850  gausslemma2dlem1a  15860  gausslemma2dlem4  15866  gausslemma2dlem5a  15867  lgseisenlem2  15873  lgsquadlem1  15879  2sqlem2  15917  mul2sq  15918  ushgredgedgloop  16152  clwwlkext2edg  16346  pw1map  16700  gsumgfsum1  16793  gsumgfsum  16796