Theorem eqtr2d 2227

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

Syntax hints:   → wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  3eqtrrd  2231  3eqtr2rd  2233  ifandc  3595  ifordc  3596  onsucmin  4539  elxp4  5153  elxp5  5154  csbopeq1a  6241  ecinxp  6664  fundmen  6860  fidifsnen  6926  sbthlemi3  7018  ctm  7168  addpinq1  7524  1idsr  7828  prsradd  7846  cnegexlem3  8196  cnegex  8197  submul2  8418  mulsubfacd  8437  divadddivap  8746  infrenegsupex  9659  xadd4d  9951  fzval3  10271  fzoshftral  10305  ceiqm1l  10382  flqdiv  10392  flqmod  10409  intqfrac  10410  modqcyc2  10431  modqdi  10463  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  seqf1oglem1  10590  seqf1oglem2  10591  seq3id2  10597  expnegzap  10644  binom2sub  10724  binom3  10728  fihashssdif  10889  reim  10996  mulreap  11008  addcj  11035  resqrexlemcalc1  11158  absimle  11228  infxrnegsupex  11406  clim2ser  11480  serf0  11495  summodclem3  11523  mptfzshft  11585  fsumrev  11586  fsum2mul  11596  isumsplit  11634  cvgratz  11675  mertenslemi1  11678  fprodrev  11762  ef4p  11837  tanval3ap  11857  efival  11875  sinmul  11887  divalglemnn  12059  dfgcd2  12151  lcmgcdlem  12215  lcm1  12219  oddpwdclemxy  12307  oddpwdclemdc  12311  eulerthlemth  12370  hashgcdeq  12377  powm2modprm  12390  pythagtriplem16  12417  pczpre  12435  pcqdiv  12445  pcadd  12478  pcfac  12488  4sqlem10  12525  4sqlem19  12547  ennnfonelemp1  12563  strslfvd  12660  xpsff1o  12932  gsumsplit1r  12981  grpinvssd  13149  grpinvval2  13155  gsumfzreidx  13407  opprrngbg  13574  opprringbg  13576  ringinvdv  13641  lss1d  13879  znzrh2  14134  cnclima  14391  divcncfap  14768  dveflem  14872  tangtx  14973  abssinper  14981  reexplog  15006  rprelogbdiv  15089  lgsdirnn0  15163  lgsdinn0  15164  gausslemma2dlem1a  15174  gausslemma2dlem4  15180  gausslemma2dlem5a  15181  lgseisenlem2  15187  lgsquadlem1  15191  2sqlem2  15202  mul2sq  15203