Theorem eqtr2d 2204

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

Syntax hints:   → wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  3eqtrrd  2208  3eqtr2rd  2210  ifandc  3563  ifordc  3564  onsucmin  4491  elxp4  5098  elxp5  5099  csbopeq1a  6167  ecinxp  6588  fundmen  6784  fidifsnen  6848  sbthlemi3  6936  ctm  7086  addpinq1  7426  1idsr  7730  prsradd  7748  cnegexlem3  8096  cnegex  8097  submul2  8318  mulsubfacd  8337  divadddivap  8644  infrenegsupex  9553  xadd4d  9842  fzval3  10160  fzoshftral  10194  ceiqm1l  10267  flqdiv  10277  flqmod  10294  intqfrac  10295  modqcyc2  10316  modqdi  10348  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  seq3id2  10465  expnegzap  10510  binom2sub  10589  binom3  10593  fihashssdif  10753  reim  10816  mulreap  10828  addcj  10855  resqrexlemcalc1  10978  absimle  11048  infxrnegsupex  11226  clim2ser  11300  serf0  11315  summodclem3  11343  mptfzshft  11405  fsumrev  11406  fsum2mul  11416  isumsplit  11454  cvgratz  11495  mertenslemi1  11498  fprodrev  11582  ef4p  11657  tanval3ap  11677  efival  11695  sinmul  11707  divalglemnn  11877  dfgcd2  11969  lcmgcdlem  12031  lcm1  12035  oddpwdclemxy  12123  oddpwdclemdc  12127  eulerthlemth  12186  hashgcdeq  12193  powm2modprm  12206  pythagtriplem16  12233  pczpre  12251  pcqdiv  12261  pcadd  12293  pcfac  12302  4sqlem10  12339  ennnfonelemp1  12361  strslfvd  12457  cnclima  13017  dveflem  13481  tangtx  13553  abssinper  13561  reexplog  13586  rprelogbdiv  13669  lgsdirnn0  13742  lgsdinn0  13743  2sqlem2  13745  mul2sq  13746