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 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  3eqtrrd  2276  3eqtr2rd  2278  ifandc  3681  ifordc  3682  onsucmin  4652  elxp4  5273  elxp5  5274  funopsn  5885  csbopeq1a  6416  ecinxp  6878  fundmen  7088  fidifsnen  7166  sbthlemi3  7270  ctm  7443  addpinq1  7825  1idsr  8129  prsradd  8147  cnegexlem3  8497  cnegex  8498  submul2  8720  mulsubfacd  8740  divadddivap  9051  infrenegsupex  9977  xadd4d  10270  fzval3  10605  fzoshftral  10640  ceiqm1l  10731  flqdiv  10741  flqmod  10758  intqfrac  10759  modqcyc2  10780  modqdi  10812  frecuzrdgtcl  10832  frecuzrdgfunlem  10839  seqf1oglem1  10939  seqf1oglem2  10940  seq3id2  10946  expnegzap  10993  binom2sub  11073  binom3  11077  resq01  11078  fihashssdif  11242  ccatw2s1p2  11397  ccats1pfxeq  11469  pfxccatin12lem2  11486  pfxccatin12  11488  swrdccat3b  11495  cats1fvnd  11520  reim  11600  mulreap  11612  addcj  11639  resqrexlemcalc1  11763  absimle  11833  infxrnegsupex  12012  clim2ser  12086  serf0  12101  summodclem3  12130  mptfzshft  12192  fsumrev  12193  fsum2mul  12203  isumsplit  12241  cvgratz  12282  mertenslemi1  12285  fprodrev  12369  ef4p  12444  tanval3ap  12464  efival  12482  sinmul  12494  divalglemnn  12668  dfgcd2  12774  lcmgcdlem  12838  lcm1  12842  oddpwdclemxy  12930  oddpwdclemdc  12934  eulerthlemth  12993  hashgcdeq  13001  powm2modprm  13014  pythagtriplem16  13041  pczpre  13059  pcqdiv  13069  pcadd  13102  pcfac  13112  4sqlem10  13149  4sqlem19  13171  ennnfonelemp1  13280  strslfvd  13377  xpsff1o  13653  gzsumsplit1r  13698  grpinvssd  13865  grpinvval2  13871  gzsumreidx  14124  gzsumshift  14132  gzsumgsum1  14136  gzsumgsum  14138  opprrngbg  14366  opprringbg  14368  ringinvdv  14435  lss1d  14703  znzrh2  14964  cnclima  15307  divcncfap  15698  dveflem  15810  plycjlemc  15844  tangtx  15922  abssinper  15930  reexplog  15955  rprelogbdiv  16042  birthdaylem2  16071  perfect1  16095  lgsdirnn0  16149  lgsdinn0  16150  gausslemma2dlem1a  16160  gausslemma2dlem4  16166  gausslemma2dlem5a  16167  lgseisenlem2  16173  lgsquadlem1  16179  2sqlem2  16217  mul2sq  16218  ushgredgedgloop  16452  clwwlkext2edg  16646  pw1map  17008