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  4654  elxp4  5275  elxp5  5276  funopsn  5891  csbopeq1a  6422  ecinxp  6884  fundmen  7094  fidifsnen  7172  sbthlemi3  7276  ctm  7449  addpinq1  7831  1idsr  8135  prsradd  8153  cnegexlem3  8503  cnegex  8504  submul2  8726  mulsubfacd  8746  divadddivap  9058  infrenegsupex  9996  xadd4d  10289  fzval3  10624  fzoshftral  10659  ceiqm1l  10750  flqdiv  10760  flqmod  10777  intqfrac  10778  modqcyc2  10799  modqdi  10831  frecuzrdgtcl  10851  frecuzrdgfunlem  10858  seqf1oglem1  10958  seqf1oglem2  10959  seq3id2  10965  expnegzap  11012  binom2sub  11092  binom3  11096  resq01  11097  fihashssdif  11261  ccatw2s1p2  11416  ccats1pfxeq  11488  pfxccatin12lem2  11505  pfxccatin12  11507  swrdccat3b  11514  cats1fvnd  11539  reim  11619  mulreap  11631  addcj  11658  resqrexlemcalc1  11782  absimle  11852  infxrnegsupex  12031  clim2ser  12105  serf0  12120  summodclem3  12149  mptfzshft  12211  fsumrev  12212  fsum2mul  12222  isumsplit  12260  cvgratz  12301  mertenslemi1  12304  fprodrev  12388  ef4p  12463  tanval3ap  12483  efival  12501  sinmul  12513  divalglemnn  12687  dfgcd2  12793  lcmgcdlem  12857  lcm1  12861  oddpwdclemxy  12949  oddpwdclemdc  12953  eulerthlemth  13012  hashgcdeq  13020  powm2modprm  13033  pythagtriplem16  13060  pczpre  13078  pcqdiv  13088  pcadd  13121  pcfac  13131  4sqlem10  13168  4sqlem19  13190  ennnfonelemp1  13299  strslfvd  13396  xpsff1o  13672  gzsumsplit1r  13717  grpinvssd  13884  grpinvval2  13890  gzsumreidx  14143  gzsumshift  14151  gzsumgsum1  14155  gzsumgsum  14157  opprrngbg  14385  opprringbg  14387  ringinvdv  14454  lss1d  14722  znzrh2  14983  cnclima  15326  divcncfap  15717  dveflem  15829  plycjlemc  15863  tangtx  15942  abssinper  15950  reexplog  15976  rprelogbdiv  16065  birthdaylem2  16094  perfect1  16118  bcp1ctr  16126  bclbnd  16127  lgsdirnn0  16178  lgsdinn0  16179  gausslemma2dlem1a  16189  gausslemma2dlem4  16195  gausslemma2dlem5a  16196  lgseisenlem2  16202  lgsquadlem1  16208  2sqlem2  16246  mul2sq  16247  ushgredgedgloop  16481  clwwlkext2edg  16675  pw1map  17037