Theorem eqtr2d 2174

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

Syntax hints:   → wi 4   = wceq 1332

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

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

This theorem is referenced by:  3eqtrrd  2178  3eqtr2rd  2180  ifandc  3513  onsucmin  4431  elxp4  5034  elxp5  5035  csbopeq1a  6094  ecinxp  6512  fundmen  6708  fidifsnen  6772  sbthlemi3  6855  ctm  7002  addpinq1  7296  1idsr  7600  prsradd  7618  cnegexlem3  7963  cnegex  7964  submul2  8185  mulsubfacd  8204  divadddivap  8511  infrenegsupex  9416  xadd4d  9698  fzval3  10012  fzoshftral  10046  ceiqm1l  10115  flqdiv  10125  flqmod  10142  intqfrac  10143  modqcyc2  10164  modqdi  10196  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  seq3id2  10313  expnegzap  10358  binom2sub  10436  binom3  10440  fihashssdif  10596  reim  10656  mulreap  10668  addcj  10695  resqrexlemcalc1  10818  absimle  10888  infxrnegsupex  11064  clim2ser  11138  serf0  11153  summodclem3  11181  mptfzshft  11243  fsumrev  11244  fsum2mul  11254  isumsplit  11292  cvgratz  11333  mertenslemi1  11336  ef4p  11437  tanval3ap  11457  efival  11475  sinmul  11487  divalglemnn  11651  dfgcd2  11738  lcmgcdlem  11794  lcm1  11798  oddpwdclemxy  11883  oddpwdclemdc  11887  hashgcdeq  11940  ennnfonelemp1  11955  strslfvd  12039  cnclima  12431  dveflem  12895  tangtx  12967  abssinper  12975  reexplog  13000  rprelogbdiv  13082