Theorem eqtr2d 2272

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtrrd  2276  3eqtr2rd  2278  ifandc  3681  ifordc  3682  onsucmin  4654  elxp4  5275  elxp5  5276  funopsn  5891  csbopeq1a  6422  ecinxp  6884  fundmen  7094  fidifsnen  7172  sbthlemi3  7276  ctm  7450  addpinq1  7832  1idsr  8136  prsradd  8154  cnegexlem3  8505  cnegex  8506  submul2  8728  mulsubfacd  8748  divadddivap  9060  infrenegsupex  10004  xadd4d  10298  fzval3  10633  fzoshftral  10668  ceiqm1l  10762  flqdiv  10772  flqmod  10789  intqfrac  10790  modqcyc2  10811  modqdi  10843  frecuzrdgtcl  10863  frecuzrdgfunlem  10870  seqf1oglem1  10970  seqf1oglem2  10971  seq3id2  10977  expnegzap  11024  binom2sub  11104  binom3  11108  resq01  11109  fihashssdif  11274  ccatw2s1p2  11429  ccats1pfxeq  11501  pfxccatin12lem2  11518  pfxccatin12  11520  swrdccat3b  11527  cats1fvnd  11552  reim  11632  mulreap  11644  addcj  11671  resqrexlemcalc1  11795  absimle  11866  infxrnegsupex  12047  clim2ser  12121  serf0  12136  summodclem3  12165  mptfzshft  12227  fsumrev  12228  fsum2mul  12238  isumsplit  12276  cvgratz  12317  mertenslemi1  12320  fprodrev  12404  ef4p  12479  tanval3ap  12499  efival  12517  sinmul  12529  divalglemnn  12703  dfgcd2  12809  lcmgcdlem  12873  lcm1  12877  nnmaxpwlemxy  12966  nnmaxpwlemparts  12970  eulerthlemth  13032  hashgcdeq  13040  powm2modprm  13053  pythagtriplem16  13080  pczpre  13098  pcqdiv  13108  pcadd  13141  pcfac  13151  4sqlem10  13188  4sqlem19  13210  ennnfonelemp1  13348  strslfvd  13445  xpsff1o  13721  gzsumsplit1r  13766  grpinvssd  13933  grpinvval2  13939  gzsumreidx  14192  gzsumshift  14200  gzsumgsum1  14204  gzsumgsum  14206  opprrngbg  14434  opprringbg  14436  ringinvdv  14503  lss1d  14771  znzrh2  15032  cnclima  15376  divcncfap  15767  dveflem  15879  plycjlemc  15913  tangtx  15992  abssinper  16000  reexplog  16026  rprelogbdiv  16115  birthdaylem2  16148  chtprm  16183  perfect1  16220  bcp1ctr  16228  bclbnd  16229  bposlem1  16233  lgsdirnn0  16288  lgsdinn0  16289  gausslemma2dlem1a  16299  gausslemma2dlem4  16305  gausslemma2dlem5a  16306  lgseisenlem2  16312  lgsquadlem1  16318  2sqlem2  16356  mul2sq  16357  ushgredgedgloop  16591  clwwlkext2edg  16785  pw1map  17147