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  3643  ifordc  3644  onsucmin  4596  elxp4  5212  elxp5  5213  funopsn  5810  csbopeq1a  6324  ecinxp  6747  fundmen  6949  fidifsnen  7020  sbthlemi3  7114  ctm  7264  addpinq1  7639  1idsr  7943  prsradd  7961  cnegexlem3  8311  cnegex  8312  submul2  8533  mulsubfacd  8553  divadddivap  8862  infrenegsupex  9777  xadd4d  10069  fzval3  10397  fzoshftral  10431  ceiqm1l  10520  flqdiv  10530  flqmod  10547  intqfrac  10548  modqcyc2  10569  modqdi  10601  frecuzrdgtcl  10621  frecuzrdgfunlem  10628  seqf1oglem1  10728  seqf1oglem2  10729  seq3id2  10735  expnegzap  10782  binom2sub  10862  binom3  10866  fihashssdif  11027  ccatw2s1p2  11162  ccats1pfxeq  11232  pfxccatin12lem2  11249  pfxccatin12  11251  swrdccat3b  11258  cats1fvnd  11283  reim  11349  mulreap  11361  addcj  11388  resqrexlemcalc1  11511  absimle  11581  infxrnegsupex  11760  clim2ser  11834  serf0  11849  summodclem3  11877  mptfzshft  11939  fsumrev  11940  fsum2mul  11950  isumsplit  11988  cvgratz  12029  mertenslemi1  12032  fprodrev  12116  ef4p  12191  tanval3ap  12211  efival  12229  sinmul  12241  divalglemnn  12415  dfgcd2  12521  lcmgcdlem  12585  lcm1  12589  oddpwdclemxy  12677  oddpwdclemdc  12681  eulerthlemth  12740  hashgcdeq  12748  powm2modprm  12761  pythagtriplem16  12788  pczpre  12806  pcqdiv  12816  pcadd  12849  pcfac  12859  4sqlem10  12896  4sqlem19  12918  ennnfonelemp1  12963  strslfvd  13060  xpsff1o  13368  gsumsplit1r  13417  grpinvssd  13596  grpinvval2  13602  gsumfzreidx  13860  opprrngbg  14027  opprringbg  14029  ringinvdv  14094  lss1d  14332  znzrh2  14595  cnclima  14882  divcncfap  15273  dveflem  15385  plycjlemc  15419  tangtx  15497  abssinper  15505  reexplog  15530  rprelogbdiv  15616  perfect1  15657  lgsdirnn0  15711  lgsdinn0  15712  gausslemma2dlem1a  15722  gausslemma2dlem4  15728  gausslemma2dlem5a  15729  lgseisenlem2  15735  lgsquadlem1  15741  2sqlem2  15779  mul2sq  15780  ushgredgedgloop  16011  pw1map  16292