Theorem eqtr2d 2266

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

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

This theorem is referenced by:  3eqtrrd  2270  3eqtr2rd  2272  ifandc  3663  ifordc  3664  onsucmin  4629  elxp4  5250  elxp5  5251  funopsn  5860  csbopeq1a  6382  ecinxp  6844  fundmen  7047  fidifsnen  7125  sbthlemi3  7229  ctm  7400  addpinq1  7779  1idsr  8083  prsradd  8101  cnegexlem3  8450  cnegex  8451  submul2  8672  mulsubfacd  8692  divadddivap  9001  infrenegsupex  9926  xadd4d  10218  fzval3  10549  fzoshftral  10584  ceiqm1l  10673  flqdiv  10683  flqmod  10700  intqfrac  10701  modqcyc2  10722  modqdi  10754  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  seqf1oglem1  10881  seqf1oglem2  10882  seq3id2  10888  expnegzap  10935  binom2sub  11015  binom3  11019  fihashssdif  11183  ccatw2s1p2  11334  ccats1pfxeq  11406  pfxccatin12lem2  11423  pfxccatin12  11425  swrdccat3b  11432  cats1fvnd  11457  reim  11537  mulreap  11549  addcj  11576  resqrexlemcalc1  11699  absimle  11769  infxrnegsupex  11948  clim2ser  12022  serf0  12037  summodclem3  12066  mptfzshft  12128  fsumrev  12129  fsum2mul  12139  isumsplit  12177  cvgratz  12218  mertenslemi1  12221  fprodrev  12305  ef4p  12380  tanval3ap  12400  efival  12418  sinmul  12430  divalglemnn  12604  dfgcd2  12710  lcmgcdlem  12774  lcm1  12778  oddpwdclemxy  12866  oddpwdclemdc  12870  eulerthlemth  12929  hashgcdeq  12937  powm2modprm  12950  pythagtriplem16  12977  pczpre  12995  pcqdiv  13005  pcadd  13038  pcfac  13048  4sqlem10  13085  4sqlem19  13107  ennnfonelemp1  13157  strslfvd  13254  xpsff1o  13562  gsumsplit1r  13611  grpinvssd  13790  grpinvval2  13796  gsumfzreidx  14054  opprrngbg  14222  opprringbg  14224  ringinvdv  14290  lss1d  14531  znzrh2  14794  cnclima  15088  divcncfap  15479  dveflem  15591  plycjlemc  15625  tangtx  15703  abssinper  15711  reexplog  15736  rprelogbdiv  15822  perfect1  15866  lgsdirnn0  15920  lgsdinn0  15921  gausslemma2dlem1a  15931  gausslemma2dlem4  15937  gausslemma2dlem5a  15938  lgseisenlem2  15944  lgsquadlem1  15950  2sqlem2  15988  mul2sq  15989  ushgredgedgloop  16223  clwwlkext2edg  16417  pw1map  16769  gsumgfsum1  16863  gsumgfsum  16866