Theorem eqtr2d 2263

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtrrd  2267  3eqtr2rd  2269  ifandc  3644  ifordc  3645  onsucmin  4603  elxp4  5222  elxp5  5223  funopsn  5825  csbopeq1a  6346  ecinxp  6774  fundmen  6976  fidifsnen  7052  sbthlemi3  7152  ctm  7302  addpinq1  7677  1idsr  7981  prsradd  7999  cnegexlem3  8349  cnegex  8350  submul2  8571  mulsubfacd  8591  divadddivap  8900  infrenegsupex  9821  xadd4d  10113  fzval3  10442  fzoshftral  10477  ceiqm1l  10566  flqdiv  10576  flqmod  10593  intqfrac  10594  modqcyc2  10615  modqdi  10647  frecuzrdgtcl  10667  frecuzrdgfunlem  10674  seqf1oglem1  10774  seqf1oglem2  10775  seq3id2  10781  expnegzap  10828  binom2sub  10908  binom3  10912  fihashssdif  11075  ccatw2s1p2  11216  ccats1pfxeq  11288  pfxccatin12lem2  11305  pfxccatin12  11307  swrdccat3b  11314  cats1fvnd  11339  reim  11406  mulreap  11418  addcj  11445  resqrexlemcalc1  11568  absimle  11638  infxrnegsupex  11817  clim2ser  11891  serf0  11906  summodclem3  11934  mptfzshft  11996  fsumrev  11997  fsum2mul  12007  isumsplit  12045  cvgratz  12086  mertenslemi1  12089  fprodrev  12173  ef4p  12248  tanval3ap  12268  efival  12286  sinmul  12298  divalglemnn  12472  dfgcd2  12578  lcmgcdlem  12642  lcm1  12646  oddpwdclemxy  12734  oddpwdclemdc  12738  eulerthlemth  12797  hashgcdeq  12805  powm2modprm  12818  pythagtriplem16  12845  pczpre  12863  pcqdiv  12873  pcadd  12906  pcfac  12916  4sqlem10  12953  4sqlem19  12975  ennnfonelemp1  13020  strslfvd  13117  xpsff1o  13425  gsumsplit1r  13474  grpinvssd  13653  grpinvval2  13659  gsumfzreidx  13917  opprrngbg  14084  opprringbg  14086  ringinvdv  14152  lss1d  14390  znzrh2  14653  cnclima  14940  divcncfap  15331  dveflem  15443  plycjlemc  15477  tangtx  15555  abssinper  15563  reexplog  15588  rprelogbdiv  15674  perfect1  15715  lgsdirnn0  15769  lgsdinn0  15770  gausslemma2dlem1a  15780  gausslemma2dlem4  15786  gausslemma2dlem5a  15787  lgseisenlem2  15793  lgsquadlem1  15799  2sqlem2  15837  mul2sq  15838  ushgredgedgloop  16072  clwwlkext2edg  16231  pw1map  16546  gsumgfsum1  16631  gsumgfsum  16634