Theorem eqtr2d 2133

Description: An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)

Hypotheses

Ref	Expression
eqtr2d.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtr2d.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
eqtr2d	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem eqtr2d

Step	Hyp	Ref	Expression
1		eqtr2d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtr2d.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	1, 2	eqtrd 2132	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2105	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1299

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082

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

This theorem is referenced by:  3eqtrrd  2137  3eqtr2rd  2139  ifandc  3455  onsucmin  4361  elxp4  4962  elxp5  4963  csbopeq1a  6016  ecinxp  6434  fundmen  6630  fidifsnen  6693  sbthlemi3  6775  ctm  6909  addpinq1  7173  1idsr  7464  prsradd  7481  cnegexlem3  7810  cnegex  7811  submul2  8028  mulsubfacd  8047  divadddivap  8348  infrenegsupex  9239  xadd4d  9509  fzval3  9822  fzoshftral  9856  ceiqm1l  9925  flqdiv  9935  flqmod  9952  intqfrac  9953  modqcyc2  9974  modqdi  10006  frecuzrdgtcl  10026  frecuzrdgfunlem  10033  seq3id2  10123  expnegzap  10168  binom2sub  10246  binom3  10250  fihashssdif  10405  reim  10465  mulreap  10477  addcj  10504  resqrexlemcalc1  10626  absimle  10696  infxrnegsupex  10871  clim2ser  10945  serf0  10960  summodclem3  10988  mptfzshft  11050  fsumrev  11051  fsum2mul  11061  isumsplit  11099  cvgratz  11140  mertenslemi1  11143  ef4p  11198  tanval3ap  11219  efival  11237  sinmul  11249  divalglemnn  11410  dfgcd2  11495  lcmgcdlem  11551  lcm1  11555  oddpwdclemxy  11639  oddpwdclemdc  11643  hashgcdeq  11696  ennnfonelemp1  11711  strslfvd  11782  cnclima  12173