Theorem eqtr2d 2265

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  3eqtrrd  2269  3eqtr2rd  2271  ifandc  3650  ifordc  3651  onsucmin  4611  elxp4  5231  elxp5  5232  funopsn  5838  csbopeq1a  6360  ecinxp  6822  fundmen  7024  fidifsnen  7100  sbthlemi3  7201  ctm  7351  addpinq1  7727  1idsr  8031  prsradd  8049  cnegexlem3  8399  cnegex  8400  submul2  8621  mulsubfacd  8641  divadddivap  8950  infrenegsupex  9871  xadd4d  10163  fzval3  10493  fzoshftral  10528  ceiqm1l  10617  flqdiv  10627  flqmod  10644  intqfrac  10645  modqcyc2  10666  modqdi  10698  frecuzrdgtcl  10718  frecuzrdgfunlem  10725  seqf1oglem1  10825  seqf1oglem2  10826  seq3id2  10832  expnegzap  10879  binom2sub  10959  binom3  10963  fihashssdif  11126  ccatw2s1p2  11270  ccats1pfxeq  11342  pfxccatin12lem2  11359  pfxccatin12  11361  swrdccat3b  11368  cats1fvnd  11393  reim  11473  mulreap  11485  addcj  11512  resqrexlemcalc1  11635  absimle  11705  infxrnegsupex  11884  clim2ser  11958  serf0  11973  summodclem3  12002  mptfzshft  12064  fsumrev  12065  fsum2mul  12075  isumsplit  12113  cvgratz  12154  mertenslemi1  12157  fprodrev  12241  ef4p  12316  tanval3ap  12336  efival  12354  sinmul  12366  divalglemnn  12540  dfgcd2  12646  lcmgcdlem  12710  lcm1  12714  oddpwdclemxy  12802  oddpwdclemdc  12806  eulerthlemth  12865  hashgcdeq  12873  powm2modprm  12886  pythagtriplem16  12913  pczpre  12931  pcqdiv  12941  pcadd  12974  pcfac  12984  4sqlem10  13021  4sqlem19  13043  ennnfonelemp1  13088  strslfvd  13185  xpsff1o  13493  gsumsplit1r  13542  grpinvssd  13721  grpinvval2  13727  gsumfzreidx  13985  opprrngbg  14153  opprringbg  14155  ringinvdv  14221  lss1d  14459  znzrh2  14722  cnclima  15014  divcncfap  15405  dveflem  15517  plycjlemc  15551  tangtx  15629  abssinper  15637  reexplog  15662  rprelogbdiv  15748  perfect1  15792  lgsdirnn0  15846  lgsdinn0  15847  gausslemma2dlem1a  15857  gausslemma2dlem4  15863  gausslemma2dlem5a  15864  lgseisenlem2  15870  lgsquadlem1  15876  2sqlem2  15914  mul2sq  15915  ushgredgedgloop  16149  clwwlkext2edg  16343  pw1map  16697  gsumgfsum1  16790  gsumgfsum  16793