Theorem eqtr2d 2230

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 2229	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2202	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtrrd  2234  3eqtr2rd  2236  ifandc  3600  ifordc  3601  onsucmin  4544  elxp4  5158  elxp5  5159  csbopeq1a  6247  ecinxp  6670  fundmen  6866  fidifsnen  6932  sbthlemi3  7026  ctm  7176  addpinq1  7533  1idsr  7837  prsradd  7855  cnegexlem3  8205  cnegex  8206  submul2  8427  mulsubfacd  8447  divadddivap  8756  infrenegsupex  9670  xadd4d  9962  fzval3  10282  fzoshftral  10316  ceiqm1l  10405  flqdiv  10415  flqmod  10432  intqfrac  10433  modqcyc2  10454  modqdi  10486  frecuzrdgtcl  10506  frecuzrdgfunlem  10513  seqf1oglem1  10613  seqf1oglem2  10614  seq3id2  10620  expnegzap  10667  binom2sub  10747  binom3  10751  fihashssdif  10912  reim  11019  mulreap  11031  addcj  11058  resqrexlemcalc1  11181  absimle  11251  infxrnegsupex  11430  clim2ser  11504  serf0  11519  summodclem3  11547  mptfzshft  11609  fsumrev  11610  fsum2mul  11620  isumsplit  11658  cvgratz  11699  mertenslemi1  11702  fprodrev  11786  ef4p  11861  tanval3ap  11881  efival  11899  sinmul  11911  divalglemnn  12085  dfgcd2  12191  lcmgcdlem  12255  lcm1  12259  oddpwdclemxy  12347  oddpwdclemdc  12351  eulerthlemth  12410  hashgcdeq  12418  powm2modprm  12431  pythagtriplem16  12458  pczpre  12476  pcqdiv  12486  pcadd  12519  pcfac  12529  4sqlem10  12566  4sqlem19  12588  ennnfonelemp1  12633  strslfvd  12730  xpsff1o  13002  gsumsplit1r  13051  grpinvssd  13219  grpinvval2  13225  gsumfzreidx  13477  opprrngbg  13644  opprringbg  13646  ringinvdv  13711  lss1d  13949  znzrh2  14212  cnclima  14469  divcncfap  14860  dveflem  14972  plycjlemc  15006  tangtx  15084  abssinper  15092  reexplog  15117  rprelogbdiv  15203  perfect1  15244  lgsdirnn0  15298  lgsdinn0  15299  gausslemma2dlem1a  15309  gausslemma2dlem4  15315  gausslemma2dlem5a  15316  lgseisenlem2  15322  lgsquadlem1  15328  2sqlem2  15366  mul2sq  15367