Theorem eqtr2d 2114

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

Syntax hints:   -> wi 4   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  3eqtrrd  2118  3eqtr2rd  2120  onsucmin  4251  elxp4  4828  elxp5  4829  csbopeq1a  5834  ecinxp  6204  fundmen  6309  fidifsnen  6355  addpinq1  6654  1idsr  6945  prsradd  6962  cnegexlem3  7285  cnegex  7286  submul2  7503  mulsubfacd  7522  divadddivap  7815  infrenegsupex  8682  fzval3  9213  fzoshftral  9247  ceiqm1l  9313  flqdiv  9323  flqmod  9340  intqfrac  9341  modqcyc2  9362  modqdi  9394  frecuzrdgfn  9414  expnegzap  9510  binom2sub  9587  binom3  9590  reim  9739  mulreap  9751  addcj  9778  resqrexlemcalc1  9900  absimle  9970  clim2iser  10175  serif0  10189  divalglemnn  10318  dfgcd2  10403  lcmgcdlem  10459  lcm1  10463  oddpwdclemxy  10547  oddpwdclemdc  10551