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  6888  fundmen  7098  fidifsnen  7176  sbthlemi3  7281  ctm  7455  addpinq1  7837  1idsr  8141  prsradd  8159  cnegexlem3  8510  cnegex  8511  submul2  8733  mulsubfacd  8753  divadddivap  9065  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  15446  divcncfap  15837  dveflem  15949  plycjlemc  15983  tangtx  16062  abssinper  16070  sineq0re  16073  reexplog  16098  rprelogbdiv  16190  birthdaylem2  16223  chtprm  16258  perfect1  16295  bcp1ctr  16303  bclbnd  16304  bposlem1  16308  lgsdirnn0  16368  lgsdinn0  16369  gausslemma2dlem1a  16379  gausslemma2dlem4  16385  gausslemma2dlem5a  16386  lgseisenlem2  16392  lgsquadlem1  16398  2sqlem2  16436  mul2sq  16437  ushgredgedgloop  16671  clwwlkext2edg  16865  pw1map  17227