Theorem eqtr2d 2199

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

Syntax hints:   → wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  3eqtrrd  2203  3eqtr2rd  2205  ifandc  3556  onsucmin  4483  elxp4  5090  elxp5  5091  csbopeq1a  6153  ecinxp  6572  fundmen  6768  fidifsnen  6832  sbthlemi3  6920  ctm  7070  addpinq1  7401  1idsr  7705  prsradd  7723  cnegexlem3  8071  cnegex  8072  submul2  8293  mulsubfacd  8312  divadddivap  8619  infrenegsupex  9528  xadd4d  9817  fzval3  10135  fzoshftral  10169  ceiqm1l  10242  flqdiv  10252  flqmod  10269  intqfrac  10270  modqcyc2  10291  modqdi  10323  frecuzrdgtcl  10343  frecuzrdgfunlem  10350  seq3id2  10440  expnegzap  10485  binom2sub  10564  binom3  10568  fihashssdif  10727  reim  10790  mulreap  10802  addcj  10829  resqrexlemcalc1  10952  absimle  11022  infxrnegsupex  11200  clim2ser  11274  serf0  11289  summodclem3  11317  mptfzshft  11379  fsumrev  11380  fsum2mul  11390  isumsplit  11428  cvgratz  11469  mertenslemi1  11472  fprodrev  11556  ef4p  11631  tanval3ap  11651  efival  11669  sinmul  11681  divalglemnn  11851  dfgcd2  11943  lcmgcdlem  12005  lcm1  12009  oddpwdclemxy  12097  oddpwdclemdc  12101  eulerthlemth  12160  hashgcdeq  12167  powm2modprm  12180  pythagtriplem16  12207  pczpre  12225  pcqdiv  12235  pcadd  12267  pcfac  12276  4sqlem10  12313  ennnfonelemp1  12335  strslfvd  12431  cnclima  12823  dveflem  13287  tangtx  13359  abssinper  13367  reexplog  13392  rprelogbdiv  13475  lgsdirnn0  13548  lgsdinn0  13549  2sqlem2  13551  mul2sq  13552