Theorem eqtr2d 2173

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

Syntax hints:   -> wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  3eqtrrd  2177  3eqtr2rd  2179  ifandc  3508  onsucmin  4423  elxp4  5026  elxp5  5027  csbopeq1a  6086  ecinxp  6504  fundmen  6700  fidifsnen  6764  sbthlemi3  6847  ctm  6994  addpinq1  7272  1idsr  7576  prsradd  7594  cnegexlem3  7939  cnegex  7940  submul2  8161  mulsubfacd  8180  divadddivap  8487  infrenegsupex  9389  xadd4d  9668  fzval3  9981  fzoshftral  10015  ceiqm1l  10084  flqdiv  10094  flqmod  10111  intqfrac  10112  modqcyc2  10133  modqdi  10165  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  seq3id2  10282  expnegzap  10327  binom2sub  10405  binom3  10409  fihashssdif  10564  reim  10624  mulreap  10636  addcj  10663  resqrexlemcalc1  10786  absimle  10856  infxrnegsupex  11032  clim2ser  11106  serf0  11121  summodclem3  11149  mptfzshft  11211  fsumrev  11212  fsum2mul  11222  isumsplit  11260  cvgratz  11301  mertenslemi1  11304  ef4p  11400  tanval3ap  11421  efival  11439  sinmul  11451  divalglemnn  11615  dfgcd2  11702  lcmgcdlem  11758  lcm1  11762  oddpwdclemxy  11847  oddpwdclemdc  11851  hashgcdeq  11904  ennnfonelemp1  11919  strslfvd  12000  cnclima  12392  dveflem  12855  tangtx  12919  abssinper  12927