Theorem eqtr2d 2240

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  3eqtrrd  2244  3eqtr2rd  2246  ifandc  3612  ifordc  3613  onsucmin  4560  elxp4  5176  elxp5  5177  funopsn  5772  csbopeq1a  6284  ecinxp  6707  fundmen  6909  fidifsnen  6979  sbthlemi3  7073  ctm  7223  addpinq1  7590  1idsr  7894  prsradd  7912  cnegexlem3  8262  cnegex  8263  submul2  8484  mulsubfacd  8504  divadddivap  8813  infrenegsupex  9728  xadd4d  10020  fzval3  10346  fzoshftral  10380  ceiqm1l  10469  flqdiv  10479  flqmod  10496  intqfrac  10497  modqcyc2  10518  modqdi  10550  frecuzrdgtcl  10570  frecuzrdgfunlem  10577  seqf1oglem1  10677  seqf1oglem2  10678  seq3id2  10684  expnegzap  10731  binom2sub  10811  binom3  10815  fihashssdif  10976  ccatw2s1p2  11111  reim  11213  mulreap  11225  addcj  11252  resqrexlemcalc1  11375  absimle  11445  infxrnegsupex  11624  clim2ser  11698  serf0  11713  summodclem3  11741  mptfzshft  11803  fsumrev  11804  fsum2mul  11814  isumsplit  11852  cvgratz  11893  mertenslemi1  11896  fprodrev  11980  ef4p  12055  tanval3ap  12075  efival  12093  sinmul  12105  divalglemnn  12279  dfgcd2  12385  lcmgcdlem  12449  lcm1  12453  oddpwdclemxy  12541  oddpwdclemdc  12545  eulerthlemth  12604  hashgcdeq  12612  powm2modprm  12625  pythagtriplem16  12652  pczpre  12670  pcqdiv  12680  pcadd  12713  pcfac  12723  4sqlem10  12760  4sqlem19  12782  ennnfonelemp1  12827  strslfvd  12924  xpsff1o  13231  gsumsplit1r  13280  grpinvssd  13459  grpinvval2  13465  gsumfzreidx  13723  opprrngbg  13890  opprringbg  13892  ringinvdv  13957  lss1d  14195  znzrh2  14458  cnclima  14745  divcncfap  15136  dveflem  15248  plycjlemc  15282  tangtx  15360  abssinper  15368  reexplog  15393  rprelogbdiv  15479  perfect1  15520  lgsdirnn0  15574  lgsdinn0  15575  gausslemma2dlem1a  15585  gausslemma2dlem4  15591  gausslemma2dlem5a  15592  lgseisenlem2  15598  lgsquadlem1  15604  2sqlem2  15642  mul2sq  15643