Theorem eqtr2d 2211

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

Syntax hints:   → wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  3eqtrrd  2215  3eqtr2rd  2217  ifandc  3574  ifordc  3575  onsucmin  4508  elxp4  5118  elxp5  5119  csbopeq1a  6191  ecinxp  6612  fundmen  6808  fidifsnen  6872  sbthlemi3  6960  ctm  7110  addpinq1  7465  1idsr  7769  prsradd  7787  cnegexlem3  8136  cnegex  8137  submul2  8358  mulsubfacd  8377  divadddivap  8686  infrenegsupex  9596  xadd4d  9887  fzval3  10206  fzoshftral  10240  ceiqm1l  10313  flqdiv  10323  flqmod  10340  intqfrac  10341  modqcyc2  10362  modqdi  10394  frecuzrdgtcl  10414  frecuzrdgfunlem  10421  seq3id2  10511  expnegzap  10556  binom2sub  10636  binom3  10640  fihashssdif  10800  reim  10863  mulreap  10875  addcj  10902  resqrexlemcalc1  11025  absimle  11095  infxrnegsupex  11273  clim2ser  11347  serf0  11362  summodclem3  11390  mptfzshft  11452  fsumrev  11453  fsum2mul  11463  isumsplit  11501  cvgratz  11542  mertenslemi1  11545  fprodrev  11629  ef4p  11704  tanval3ap  11724  efival  11742  sinmul  11754  divalglemnn  11925  dfgcd2  12017  lcmgcdlem  12079  lcm1  12083  oddpwdclemxy  12171  oddpwdclemdc  12175  eulerthlemth  12234  hashgcdeq  12241  powm2modprm  12254  pythagtriplem16  12281  pczpre  12299  pcqdiv  12309  pcadd  12341  pcfac  12350  4sqlem10  12387  ennnfonelemp1  12409  strslfvd  12506  xpsff1o  12773  grpinvssd  12952  grpinvval2  12958  opprringbg  13255  ringinvdv  13319  lss1d  13475  cnclima  13762  dveflem  14226  tangtx  14298  abssinper  14306  reexplog  14331  rprelogbdiv  14414  lgsdirnn0  14487  lgsdinn0  14488  lgseisenlem2  14490  2sqlem2  14501  mul2sq  14502