Theorem eqtr2d 2266

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  3eqtrrd  2270  3eqtr2rd  2272  ifandc  3662  ifordc  3663  onsucmin  4628  elxp4  5249  elxp5  5250  funopsn  5859  csbopeq1a  6381  ecinxp  6843  fundmen  7046  fidifsnen  7124  sbthlemi3  7228  ctm  7399  addpinq1  7778  1idsr  8082  prsradd  8100  cnegexlem3  8449  cnegex  8450  submul2  8671  mulsubfacd  8691  divadddivap  9000  infrenegsupex  9925  xadd4d  10217  fzval3  10548  fzoshftral  10583  ceiqm1l  10672  flqdiv  10682  flqmod  10699  intqfrac  10700  modqcyc2  10721  modqdi  10753  frecuzrdgtcl  10773  frecuzrdgfunlem  10780  seqf1oglem1  10880  seqf1oglem2  10881  seq3id2  10887  expnegzap  10934  binom2sub  11014  binom3  11018  fihashssdif  11181  ccatw2s1p2  11330  ccats1pfxeq  11402  pfxccatin12lem2  11419  pfxccatin12  11421  swrdccat3b  11428  cats1fvnd  11453  reim  11533  mulreap  11545  addcj  11572  resqrexlemcalc1  11695  absimle  11765  infxrnegsupex  11944  clim2ser  12018  serf0  12033  summodclem3  12062  mptfzshft  12124  fsumrev  12125  fsum2mul  12135  isumsplit  12173  cvgratz  12214  mertenslemi1  12217  fprodrev  12301  ef4p  12376  tanval3ap  12396  efival  12414  sinmul  12426  divalglemnn  12600  dfgcd2  12706  lcmgcdlem  12770  lcm1  12774  oddpwdclemxy  12862  oddpwdclemdc  12866  eulerthlemth  12925  hashgcdeq  12933  powm2modprm  12946  pythagtriplem16  12973  pczpre  12991  pcqdiv  13001  pcadd  13034  pcfac  13044  4sqlem10  13081  4sqlem19  13103  ennnfonelemp1  13149  strslfvd  13246  xpsff1o  13554  gsumsplit1r  13603  grpinvssd  13782  grpinvval2  13788  gsumfzreidx  14046  opprrngbg  14214  opprringbg  14216  ringinvdv  14282  lss1d  14523  znzrh2  14786  cnclima  15080  divcncfap  15471  dveflem  15583  plycjlemc  15617  tangtx  15695  abssinper  15703  reexplog  15728  rprelogbdiv  15814  perfect1  15858  lgsdirnn0  15912  lgsdinn0  15913  gausslemma2dlem1a  15923  gausslemma2dlem4  15929  gausslemma2dlem5a  15930  lgseisenlem2  15936  lgsquadlem1  15942  2sqlem2  15980  mul2sq  15981  ushgredgedgloop  16215  clwwlkext2edg  16409  pw1map  16761  gsumgfsum1  16854  gsumgfsum  16857