Theorem eqtr2d 2268

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 2267	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2240	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 2216

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

This theorem is referenced by:  3eqtrrd  2272  3eqtr2rd  2274  ifandc  3667  ifordc  3668  onsucmin  4634  elxp4  5255  elxp5  5256  funopsn  5865  csbopeq1a  6395  ecinxp  6857  fundmen  7060  fidifsnen  7138  sbthlemi3  7242  ctm  7413  addpinq1  7795  1idsr  8099  prsradd  8117  cnegexlem3  8466  cnegex  8467  submul2  8689  mulsubfacd  8709  divadddivap  9018  infrenegsupex  9944  xadd4d  10237  fzval3  10571  fzoshftral  10606  ceiqm1l  10697  flqdiv  10707  flqmod  10724  intqfrac  10725  modqcyc2  10746  modqdi  10778  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  seqf1oglem1  10905  seqf1oglem2  10906  seq3id2  10912  expnegzap  10959  binom2sub  11039  binom3  11043  resq01  11044  fihashssdif  11208  ccatw2s1p2  11359  ccats1pfxeq  11431  pfxccatin12lem2  11448  pfxccatin12  11450  swrdccat3b  11457  cats1fvnd  11482  reim  11562  mulreap  11574  addcj  11601  resqrexlemcalc1  11724  absimle  11794  infxrnegsupex  11973  clim2ser  12047  serf0  12062  summodclem3  12091  mptfzshft  12153  fsumrev  12154  fsum2mul  12164  isumsplit  12202  cvgratz  12243  mertenslemi1  12246  fprodrev  12330  ef4p  12405  tanval3ap  12425  efival  12443  sinmul  12455  divalglemnn  12629  dfgcd2  12735  lcmgcdlem  12799  lcm1  12803  oddpwdclemxy  12891  oddpwdclemdc  12895  eulerthlemth  12954  hashgcdeq  12962  powm2modprm  12975  pythagtriplem16  13002  pczpre  13020  pcqdiv  13030  pcadd  13063  pcfac  13073  4sqlem10  13110  4sqlem19  13132  ennnfonelemp1  13241  strslfvd  13338  xpsff1o  13646  gsumsplit1r  13695  grpinvssd  13874  grpinvval2  13880  gsumfzreidx  14138  opprrngbg  14306  opprringbg  14308  ringinvdv  14375  lss1d  14643  znzrh2  14906  cnclima  15200  divcncfap  15591  dveflem  15703  plycjlemc  15737  tangtx  15815  abssinper  15823  reexplog  15848  rprelogbdiv  15934  perfect1  15978  lgsdirnn0  16032  lgsdinn0  16033  gausslemma2dlem1a  16043  gausslemma2dlem4  16049  gausslemma2dlem5a  16050  lgseisenlem2  16056  lgsquadlem1  16062  2sqlem2  16100  mul2sq  16101  ushgredgedgloop  16335  clwwlkext2edg  16529  pw1map  16881  gsumgfsum1  16975  gsumgfsum  16978