Theorem eqtr2d 2263

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222

This theorem is referenced by:  3eqtrrd  2267  3eqtr2rd  2269  ifandc  3643  ifordc  3644  onsucmin  4599  elxp4  5216  elxp5  5217  funopsn  5819  csbopeq1a  6340  ecinxp  6765  fundmen  6967  fidifsnen  7040  sbthlemi3  7134  ctm  7284  addpinq1  7659  1idsr  7963  prsradd  7981  cnegexlem3  8331  cnegex  8332  submul2  8553  mulsubfacd  8573  divadddivap  8882  infrenegsupex  9797  xadd4d  10089  fzval3  10418  fzoshftral  10452  ceiqm1l  10541  flqdiv  10551  flqmod  10568  intqfrac  10569  modqcyc2  10590  modqdi  10622  frecuzrdgtcl  10642  frecuzrdgfunlem  10649  seqf1oglem1  10749  seqf1oglem2  10750  seq3id2  10756  expnegzap  10803  binom2sub  10883  binom3  10887  fihashssdif  11048  ccatw2s1p2  11184  ccats1pfxeq  11254  pfxccatin12lem2  11271  pfxccatin12  11273  swrdccat3b  11280  cats1fvnd  11305  reim  11371  mulreap  11383  addcj  11410  resqrexlemcalc1  11533  absimle  11603  infxrnegsupex  11782  clim2ser  11856  serf0  11871  summodclem3  11899  mptfzshft  11961  fsumrev  11962  fsum2mul  11972  isumsplit  12010  cvgratz  12051  mertenslemi1  12054  fprodrev  12138  ef4p  12213  tanval3ap  12233  efival  12251  sinmul  12263  divalglemnn  12437  dfgcd2  12543  lcmgcdlem  12607  lcm1  12611  oddpwdclemxy  12699  oddpwdclemdc  12703  eulerthlemth  12762  hashgcdeq  12770  powm2modprm  12783  pythagtriplem16  12810  pczpre  12828  pcqdiv  12838  pcadd  12871  pcfac  12881  4sqlem10  12918  4sqlem19  12940  ennnfonelemp1  12985  strslfvd  13082  xpsff1o  13390  gsumsplit1r  13439  grpinvssd  13618  grpinvval2  13624  gsumfzreidx  13882  opprrngbg  14049  opprringbg  14051  ringinvdv  14117  lss1d  14355  znzrh2  14618  cnclima  14905  divcncfap  15296  dveflem  15408  plycjlemc  15442  tangtx  15520  abssinper  15528  reexplog  15553  rprelogbdiv  15639  perfect1  15680  lgsdirnn0  15734  lgsdinn0  15735  gausslemma2dlem1a  15745  gausslemma2dlem4  15751  gausslemma2dlem5a  15752  lgseisenlem2  15758  lgsquadlem1  15764  2sqlem2  15802  mul2sq  15803  ushgredgedgloop  16034  pw1map  16390