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  3573  ifordc  3574  onsucmin  4507  elxp4  5117  elxp5  5118  csbopeq1a  6189  ecinxp  6610  fundmen  6806  fidifsnen  6870  sbthlemi3  6958  ctm  7108  addpinq1  7463  1idsr  7767  prsradd  7785  cnegexlem3  8134  cnegex  8135  submul2  8356  mulsubfacd  8375  divadddivap  8684  infrenegsupex  9594  xadd4d  9885  fzval3  10204  fzoshftral  10238  ceiqm1l  10311  flqdiv  10321  flqmod  10338  intqfrac  10339  modqcyc2  10360  modqdi  10392  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  seq3id2  10509  expnegzap  10554  binom2sub  10634  binom3  10638  fihashssdif  10798  reim  10861  mulreap  10873  addcj  10900  resqrexlemcalc1  11023  absimle  11093  infxrnegsupex  11271  clim2ser  11345  serf0  11360  summodclem3  11388  mptfzshft  11450  fsumrev  11451  fsum2mul  11461  isumsplit  11499  cvgratz  11540  mertenslemi1  11543  fprodrev  11627  ef4p  11702  tanval3ap  11722  efival  11740  sinmul  11752  divalglemnn  11923  dfgcd2  12015  lcmgcdlem  12077  lcm1  12081  oddpwdclemxy  12169  oddpwdclemdc  12173  eulerthlemth  12232  hashgcdeq  12239  powm2modprm  12252  pythagtriplem16  12279  pczpre  12297  pcqdiv  12307  pcadd  12339  pcfac  12348  4sqlem10  12385  ennnfonelemp1  12407  strslfvd  12504  xpsff1o  12768  grpinvssd  12947  grpinvval2  12953  opprringbg  13250  ringinvdv  13314  cnclima  13726  dveflem  14190  tangtx  14262  abssinper  14270  reexplog  14295  rprelogbdiv  14378  lgsdirnn0  14451  lgsdinn0  14452  lgseisenlem2  14454  2sqlem2  14465  mul2sq  14466