Theorem eqtr2d 2115

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

Syntax hints:   → wi 4   = wceq 1285

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-cleq 2075

This theorem is referenced by:  3eqtrrd  2119  3eqtr2rd  2121  onsucmin  4259  elxp4  4838  elxp5  4839  csbopeq1a  5845  ecinxp  6247  fundmen  6353  fidifsnen  6405  addpinq1  6716  1idsr  7007  prsradd  7024  cnegexlem3  7352  cnegex  7353  submul2  7570  mulsubfacd  7589  divadddivap  7882  infrenegsupex  8763  fzval3  9290  fzoshftral  9324  ceiqm1l  9393  flqdiv  9403  flqmod  9420  intqfrac  9421  modqcyc2  9442  modqdi  9474  frecuzrdgtcl  9494  frecuzrdgfunlem  9501  iseqid2  9564  expnegzap  9607  binom2sub  9684  binom3  9687  reim  9877  mulreap  9889  addcj  9916  resqrexlemcalc1  10038  absimle  10108  clim2iser  10313  serif0  10327  divalglemnn  10462  dfgcd2  10547  lcmgcdlem  10603  lcm1  10607  oddpwdclemxy  10691  oddpwdclemdc  10695