Theorem eqtr2d 2268

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 2267	. 2 |- ( ph -> A = C )
4	3	eqcomd 2240	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 2216

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

This theorem is referenced by:  3eqtrrd  2272  3eqtr2rd  2274  ifandc  3667  ifordc  3668  onsucmin  4634  elxp4  5255  elxp5  5256  funopsn  5865  csbopeq1a  6395  ecinxp  6857  fundmen  7060  fidifsnen  7138  sbthlemi3  7242  ctm  7413  addpinq1  7795  1idsr  8099  prsradd  8117  cnegexlem3  8466  cnegex  8467  submul2  8689  mulsubfacd  8709  divadddivap  9018  infrenegsupex  9944  xadd4d  10237  fzval3  10571  fzoshftral  10606  ceiqm1l  10697  flqdiv  10707  flqmod  10724  intqfrac  10725  modqcyc2  10746  modqdi  10778  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  seqf1oglem1  10905  seqf1oglem2  10906  seq3id2  10912  expnegzap  10959  binom2sub  11039  binom3  11043  resq01  11044  fihashssdif  11208  ccatw2s1p2  11359  ccats1pfxeq  11431  pfxccatin12lem2  11448  pfxccatin12  11450  swrdccat3b  11457  cats1fvnd  11482  reim  11562  mulreap  11574  addcj  11601  resqrexlemcalc1  11724  absimle  11794  infxrnegsupex  11973  clim2ser  12047  serf0  12062  summodclem3  12091  mptfzshft  12153  fsumrev  12154  fsum2mul  12164  isumsplit  12202  cvgratz  12243  mertenslemi1  12246  fprodrev  12330  ef4p  12405  tanval3ap  12425  efival  12443  sinmul  12455  divalglemnn  12629  dfgcd2  12735  lcmgcdlem  12799  lcm1  12803  oddpwdclemxy  12891  oddpwdclemdc  12895  eulerthlemth  12954  hashgcdeq  12962  powm2modprm  12975  pythagtriplem16  13002  pczpre  13020  pcqdiv  13030  pcadd  13063  pcfac  13073  4sqlem10  13110  4sqlem19  13132  ennnfonelemp1  13241  strslfvd  13338  xpsff1o  13613  gsumsplit1r  13661  grpinvssd  13832  grpinvval2  13838  gsumfzreidx  14090  gsumgfsum1  14103  gsumgfsum  14106  opprrngbg  14321  opprringbg  14323  ringinvdv  14390  lss1d  14657  znzrh2  14920  cnclima  15214  divcncfap  15605  dveflem  15717  plycjlemc  15751  tangtx  15829  abssinper  15837  reexplog  15862  rprelogbdiv  15948  perfect1  15992  lgsdirnn0  16046  lgsdinn0  16047  gausslemma2dlem1a  16057  gausslemma2dlem4  16063  gausslemma2dlem5a  16064  lgseisenlem2  16070  lgsquadlem1  16076  2sqlem2  16114  mul2sq  16115  ushgredgedgloop  16349  clwwlkext2edg  16543  pw1map  16895