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  8467  cnegex  8468  submul2  8690  mulsubfacd  8710  divadddivap  9021  infrenegsupex  9947  xadd4d  10240  fzval3  10574  fzoshftral  10609  ceiqm1l  10700  flqdiv  10710  flqmod  10727  intqfrac  10728  modqcyc2  10749  modqdi  10781  frecuzrdgtcl  10801  frecuzrdgfunlem  10808  seqf1oglem1  10908  seqf1oglem2  10909  seq3id2  10915  expnegzap  10962  binom2sub  11042  binom3  11046  resq01  11047  fihashssdif  11211  ccatw2s1p2  11362  ccats1pfxeq  11434  pfxccatin12lem2  11451  pfxccatin12  11453  swrdccat3b  11460  cats1fvnd  11485  reim  11565  mulreap  11577  addcj  11604  resqrexlemcalc1  11728  absimle  11798  infxrnegsupex  11977  clim2ser  12051  serf0  12066  summodclem3  12095  mptfzshft  12157  fsumrev  12158  fsum2mul  12168  isumsplit  12206  cvgratz  12247  mertenslemi1  12250  fprodrev  12334  ef4p  12409  tanval3ap  12429  efival  12447  sinmul  12459  divalglemnn  12633  dfgcd2  12739  lcmgcdlem  12803  lcm1  12807  oddpwdclemxy  12895  oddpwdclemdc  12899  eulerthlemth  12958  hashgcdeq  12966  powm2modprm  12979  pythagtriplem16  13006  pczpre  13024  pcqdiv  13034  pcadd  13067  pcfac  13077  4sqlem10  13114  4sqlem19  13136  ennnfonelemp1  13245  strslfvd  13342  xpsff1o  13617  gsumsplit1r  13665  grpinvssd  13836  grpinvval2  13842  gsumfzreidx  14094  gsumgfsum1  14107  gsumgfsum  14110  opprrngbg  14325  opprringbg  14327  ringinvdv  14394  lss1d  14661  znzrh2  14924  cnclima  15218  divcncfap  15609  dveflem  15721  plycjlemc  15755  tangtx  15833  abssinper  15841  reexplog  15866  rprelogbdiv  15952  perfect1  15996  lgsdirnn0  16050  lgsdinn0  16051  gausslemma2dlem1a  16061  gausslemma2dlem4  16067  gausslemma2dlem5a  16068  lgseisenlem2  16074  lgsquadlem1  16080  2sqlem2  16118  mul2sq  16119  ushgredgedgloop  16353  clwwlkext2edg  16547  pw1map  16909