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  4600  elxp4  5219  elxp5  5220  funopsn  5822  csbopeq1a  6343  ecinxp  6770  fundmen  6972  fidifsnen  7045  sbthlemi3  7142  ctm  7292  addpinq1  7667  1idsr  7971  prsradd  7989  cnegexlem3  8339  cnegex  8340  submul2  8561  mulsubfacd  8581  divadddivap  8890  infrenegsupex  9806  xadd4d  10098  fzval3  10427  fzoshftral  10461  ceiqm1l  10550  flqdiv  10560  flqmod  10577  intqfrac  10578  modqcyc2  10599  modqdi  10631  frecuzrdgtcl  10651  frecuzrdgfunlem  10658  seqf1oglem1  10758  seqf1oglem2  10759  seq3id2  10765  expnegzap  10812  binom2sub  10892  binom3  10896  fihashssdif  11058  ccatw2s1p2  11197  ccats1pfxeq  11267  pfxccatin12lem2  11284  pfxccatin12  11286  swrdccat3b  11293  cats1fvnd  11318  reim  11384  mulreap  11396  addcj  11423  resqrexlemcalc1  11546  absimle  11616  infxrnegsupex  11795  clim2ser  11869  serf0  11884  summodclem3  11912  mptfzshft  11974  fsumrev  11975  fsum2mul  11985  isumsplit  12023  cvgratz  12064  mertenslemi1  12067  fprodrev  12151  ef4p  12226  tanval3ap  12246  efival  12264  sinmul  12276  divalglemnn  12450  dfgcd2  12556  lcmgcdlem  12620  lcm1  12624  oddpwdclemxy  12712  oddpwdclemdc  12716  eulerthlemth  12775  hashgcdeq  12783  powm2modprm  12796  pythagtriplem16  12823  pczpre  12841  pcqdiv  12851  pcadd  12884  pcfac  12894  4sqlem10  12931  4sqlem19  12953  ennnfonelemp1  12998  strslfvd  13095  xpsff1o  13403  gsumsplit1r  13452  grpinvssd  13631  grpinvval2  13637  gsumfzreidx  13895  opprrngbg  14062  opprringbg  14064  ringinvdv  14130  lss1d  14368  znzrh2  14631  cnclima  14918  divcncfap  15309  dveflem  15421  plycjlemc  15455  tangtx  15533  abssinper  15541  reexplog  15566  rprelogbdiv  15652  perfect1  15693  lgsdirnn0  15747  lgsdinn0  15748  gausslemma2dlem1a  15758  gausslemma2dlem4  15764  gausslemma2dlem5a  15765  lgseisenlem2  15771  lgsquadlem1  15777  2sqlem2  15815  mul2sq  15816  ushgredgedgloop  16047  clwwlkext2edg  16190  pw1map  16474