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  4656  elxp4  5278  elxp5  5279  funopsn  5894  csbopeq1a  6426  ecinxp  6889  fundmen  7100  fidifsnen  7178  sbthlemi3  7283  ctm  7456  addpinq1  7838  1idsr  8142  prsradd  8160  cnegexlem3  8511  cnegex  8512  submul2  8734  mulsubfacd  8754  divadddivap  9066  infrenegsupex  10010  xadd4d  10304  fzval3  10639  fzoshftral  10674  ceiqm1l  10769  flqdiv  10779  flqmod  10796  intqfrac  10797  modqcyc2  10818  modqdi  10850  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  seqf1oglem1  10977  seqf1oglem2  10978  seq3id2  10984  expnegzap  11031  binom2sub  11111  binom3  11115  resq01  11116  fihashssdif  11281  ccatw2s1p2  11436  ccats1pfxeq  11508  pfxccatin12lem2  11525  pfxccatin12  11527  swrdccat3b  11534  cats1fvnd  11559  reim  11639  mulreap  11651  addcj  11678  resqrexlemcalc1  11802  absimle  11873  infxrnegsupex  12054  clim2ser  12128  serf0  12143  summodclem3  12172  mptfzshft  12234  fsumrev  12235  fsum2mul  12245  isumsplit  12283  cvgratz  12324  mertenslemi1  12327  fprodrev  12411  ef4p  12486  tanval3ap  12506  efival  12524  sinmul  12536  divalglemnn  12710  dfgcd2  12816  lcmgcdlem  12880  lcm1  12884  nnmaxpwlemxy  12973  nnmaxpwlemparts  12977  eulerthlemth  13039  hashgcdeq  13047  powm2modprm  13060  pythagtriplem16  13087  pczpre  13105  pcqdiv  13115  pcadd  13148  pcfac  13158  4sqlem10  13195  4sqlem19  13217  ennnfonelemp1  13355  strslfvd  13452  xpsff1o  13729  gzsumsplit1r  13774  grpinvssd  13941  grpinvval2  13947  gzsumreidx  14231  gzsumshift  14239  gzsumgsum1  14243  gzsumgsum  14245  opprrngbg  14492  opprringbg  14494  ringinvdv  14561  lss1d  14829  znzrh2  15090  cnclima  15482  divcncfap  15873  dveflem  15985  plycjlemc  16019  tangtx  16098  abssinper  16106  sineq0re  16109  reexplog  16134  rprelogbdiv  16226  birthdaylem2  16259  chtprm  16294  perfect1  16331  bcp1ctr  16339  bclbnd  16340  bposlem1  16344  lgsdirnn0  16404  lgsdinn0  16405  gausslemma2dlem1a  16415  gausslemma2dlem4  16421  gausslemma2dlem5a  16422  lgseisenlem2  16428  lgsquadlem1  16434  2sqlem2  16472  mul2sq  16473  ushgredgedgloop  16707  clwwlkext2edg  16901  pw1map  17263