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  7099  fidifsnen  7177  sbthlemi3  7282  ctm  7456  addpinq1  7838  1idsr  8142  prsradd  8160  cnegexlem3  8511  cnegex  8512  submul2  8734  mulsubfacd  8754  divadddivap  9066  infrenegsupex  10011  xadd4d  10305  fzval3  10640  fzoshftral  10675  ceiqm1l  10770  flqdiv  10780  flqmod  10797  intqfrac  10798  modqcyc2  10819  modqdi  10851  frecuzrdgtcl  10871  frecuzrdgfunlem  10878  seqf1oglem1  10978  seqf1oglem2  10979  seq3id2  10985  expnegzap  11032  binom2sub  11112  binom3  11116  resq01  11117  fihashssdif  11282  ccatw2s1p2  11437  ccats1pfxeq  11509  pfxccatin12lem2  11526  pfxccatin12  11528  swrdccat3b  11535  cats1fvnd  11560  reim  11640  mulreap  11652  addcj  11679  resqrexlemcalc1  11803  absimle  11874  infxrnegsupex  12055  clim2ser  12129  serf0  12144  summodclem3  12173  mptfzshft  12235  fsumrev  12236  fsum2mul  12246  isumsplit  12284  cvgratz  12325  mertenslemi1  12328  fprodrev  12412  ef4p  12487  tanval3ap  12507  efival  12525  sinmul  12537  divalglemnn  12711  dfgcd2  12817  lcmgcdlem  12881  lcm1  12885  nnmaxpwlemxy  12974  nnmaxpwlemparts  12978  eulerthlemth  13040  hashgcdeq  13048  powm2modprm  13061  pythagtriplem16  13088  pczpre  13106  pcqdiv  13116  pcadd  13149  pcfac  13159  4sqlem10  13196  4sqlem19  13218  ennnfonelemp1  13356  strslfvd  13453  xpsff1o  13730  gzsumsplit1r  13775  grpinvssd  13942  grpinvval2  13948  gzsumreidx  14232  gzsumshift  14240  gzsumgsum1  14244  gzsumgsum  14246  opprrngbg  14493  opprringbg  14495  ringinvdv  14562  lss1d  14830  znzrh2  15091  cnclima  15461  divcncfap  15852  dveflem  15964  plycjlemc  15998  tangtx  16077  abssinper  16085  sineq0re  16088  reexplog  16113  rprelogbdiv  16205  birthdaylem2  16238  chtprm  16273  perfect1  16310  bcp1ctr  16318  bclbnd  16319  bposlem1  16323  lgsdirnn0  16383  lgsdinn0  16384  gausslemma2dlem1a  16394  gausslemma2dlem4  16400  gausslemma2dlem5a  16401  lgseisenlem2  16407  lgsquadlem1  16413  2sqlem2  16451  mul2sq  16452  ushgredgedgloop  16686  clwwlkext2edg  16880  pw1map  17242