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  4598  elxp4  5215  elxp5  5216  funopsn  5816  csbopeq1a  6332  ecinxp  6755  fundmen  6957  fidifsnen  7028  sbthlemi3  7122  ctm  7272  addpinq1  7647  1idsr  7951  prsradd  7969  cnegexlem3  8319  cnegex  8320  submul2  8541  mulsubfacd  8561  divadddivap  8870  infrenegsupex  9785  xadd4d  10077  fzval3  10405  fzoshftral  10439  ceiqm1l  10528  flqdiv  10538  flqmod  10555  intqfrac  10556  modqcyc2  10577  modqdi  10609  frecuzrdgtcl  10629  frecuzrdgfunlem  10636  seqf1oglem1  10736  seqf1oglem2  10737  seq3id2  10743  expnegzap  10790  binom2sub  10870  binom3  10874  fihashssdif  11035  ccatw2s1p2  11171  ccats1pfxeq  11241  pfxccatin12lem2  11258  pfxccatin12  11260  swrdccat3b  11267  cats1fvnd  11292  reim  11358  mulreap  11370  addcj  11397  resqrexlemcalc1  11520  absimle  11590  infxrnegsupex  11769  clim2ser  11843  serf0  11858  summodclem3  11886  mptfzshft  11948  fsumrev  11949  fsum2mul  11959  isumsplit  11997  cvgratz  12038  mertenslemi1  12041  fprodrev  12125  ef4p  12200  tanval3ap  12220  efival  12238  sinmul  12250  divalglemnn  12424  dfgcd2  12530  lcmgcdlem  12594  lcm1  12598  oddpwdclemxy  12686  oddpwdclemdc  12690  eulerthlemth  12749  hashgcdeq  12757  powm2modprm  12770  pythagtriplem16  12797  pczpre  12815  pcqdiv  12825  pcadd  12858  pcfac  12868  4sqlem10  12905  4sqlem19  12927  ennnfonelemp1  12972  strslfvd  13069  xpsff1o  13377  gsumsplit1r  13426  grpinvssd  13605  grpinvval2  13611  gsumfzreidx  13869  opprrngbg  14036  opprringbg  14038  ringinvdv  14103  lss1d  14341  znzrh2  14604  cnclima  14891  divcncfap  15282  dveflem  15394  plycjlemc  15428  tangtx  15506  abssinper  15514  reexplog  15539  rprelogbdiv  15625  perfect1  15666  lgsdirnn0  15720  lgsdinn0  15721  gausslemma2dlem1a  15731  gausslemma2dlem4  15737  gausslemma2dlem5a  15738  lgseisenlem2  15744  lgsquadlem1  15750  2sqlem2  15788  mul2sq  15789  ushgredgedgloop  16020  pw1map  16320