Theorem eqtr2d 2265

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

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  3eqtrrd  2269  3eqtr2rd  2271  ifandc  3646  ifordc  3647  onsucmin  4605  elxp4  5224  elxp5  5225  funopsn  5830  csbopeq1a  6351  ecinxp  6779  fundmen  6981  fidifsnen  7057  sbthlemi3  7158  ctm  7308  addpinq1  7684  1idsr  7988  prsradd  8006  cnegexlem3  8356  cnegex  8357  submul2  8578  mulsubfacd  8598  divadddivap  8907  infrenegsupex  9828  xadd4d  10120  fzval3  10449  fzoshftral  10484  ceiqm1l  10573  flqdiv  10583  flqmod  10600  intqfrac  10601  modqcyc2  10622  modqdi  10654  frecuzrdgtcl  10674  frecuzrdgfunlem  10681  seqf1oglem1  10781  seqf1oglem2  10782  seq3id2  10788  expnegzap  10835  binom2sub  10915  binom3  10919  fihashssdif  11082  ccatw2s1p2  11223  ccats1pfxeq  11295  pfxccatin12lem2  11312  pfxccatin12  11314  swrdccat3b  11321  cats1fvnd  11346  reim  11413  mulreap  11425  addcj  11452  resqrexlemcalc1  11575  absimle  11645  infxrnegsupex  11824  clim2ser  11898  serf0  11913  summodclem3  11942  mptfzshft  12004  fsumrev  12005  fsum2mul  12015  isumsplit  12053  cvgratz  12094  mertenslemi1  12097  fprodrev  12181  ef4p  12256  tanval3ap  12276  efival  12294  sinmul  12306  divalglemnn  12480  dfgcd2  12586  lcmgcdlem  12650  lcm1  12654  oddpwdclemxy  12742  oddpwdclemdc  12746  eulerthlemth  12805  hashgcdeq  12813  powm2modprm  12826  pythagtriplem16  12853  pczpre  12871  pcqdiv  12881  pcadd  12914  pcfac  12924  4sqlem10  12961  4sqlem19  12983  ennnfonelemp1  13028  strslfvd  13125  xpsff1o  13433  gsumsplit1r  13482  grpinvssd  13661  grpinvval2  13667  gsumfzreidx  13925  opprrngbg  14093  opprringbg  14095  ringinvdv  14161  lss1d  14399  znzrh2  14662  cnclima  14949  divcncfap  15340  dveflem  15452  plycjlemc  15486  tangtx  15564  abssinper  15572  reexplog  15597  rprelogbdiv  15683  perfect1  15724  lgsdirnn0  15778  lgsdinn0  15779  gausslemma2dlem1a  15789  gausslemma2dlem4  15795  gausslemma2dlem5a  15796  lgseisenlem2  15802  lgsquadlem1  15808  2sqlem2  15846  mul2sq  15847  ushgredgedgloop  16081  clwwlkext2edg  16275  pw1map  16599  gsumgfsum1  16684  gsumgfsum  16687