Theorem eqtr2d 2073

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

Syntax hints:   → wi 4   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  3eqtrrd  2077  3eqtr2rd  2079  onsucmin  4233  elxp4  4808  elxp5  4809  csbopeq1a  5814  ecinxp  6181  fundmen  6286  fidifsnen  6331  addpinq1  6562  1idsr  6853  prsradd  6870  cnegexlem3  7188  cnegex  7189  submul2  7396  mulsubfacd  7415  divadddivap  7703  fzval3  9060  fzoshftral  9094  ceiqm1l  9153  flqdiv  9163  flqmod  9180  intqfrac  9181  frecuzrdgfn  9198  expnegzap  9289  binom2sub  9364  binom3  9366  reim  9452  mulreap  9464  addcj  9491  resqrexlemcalc1  9612  absimle  9680  clim2iser  9857  serif0  9871