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  10450  fzoshftral  10485  ceiqm1l  10574  flqdiv  10584  flqmod  10601  intqfrac  10602  modqcyc2  10623  modqdi  10655  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  seqf1oglem1  10782  seqf1oglem2  10783  seq3id2  10789  expnegzap  10836  binom2sub  10916  binom3  10920  fihashssdif  11083  ccatw2s1p2  11227  ccats1pfxeq  11299  pfxccatin12lem2  11316  pfxccatin12  11318  swrdccat3b  11325  cats1fvnd  11350  reim  11417  mulreap  11429  addcj  11456  resqrexlemcalc1  11579  absimle  11649  infxrnegsupex  11828  clim2ser  11902  serf0  11917  summodclem3  11946  mptfzshft  12008  fsumrev  12009  fsum2mul  12019  isumsplit  12057  cvgratz  12098  mertenslemi1  12101  fprodrev  12185  ef4p  12260  tanval3ap  12280  efival  12298  sinmul  12310  divalglemnn  12484  dfgcd2  12590  lcmgcdlem  12654  lcm1  12658  oddpwdclemxy  12746  oddpwdclemdc  12750  eulerthlemth  12809  hashgcdeq  12817  powm2modprm  12830  pythagtriplem16  12857  pczpre  12875  pcqdiv  12885  pcadd  12918  pcfac  12928  4sqlem10  12965  4sqlem19  12987  ennnfonelemp1  13032  strslfvd  13129  xpsff1o  13437  gsumsplit1r  13486  grpinvssd  13665  grpinvval2  13671  gsumfzreidx  13929  opprrngbg  14097  opprringbg  14099  ringinvdv  14165  lss1d  14403  znzrh2  14666  cnclima  14953  divcncfap  15344  dveflem  15456  plycjlemc  15490  tangtx  15568  abssinper  15576  reexplog  15601  rprelogbdiv  15687  perfect1  15728  lgsdirnn0  15782  lgsdinn0  15783  gausslemma2dlem1a  15793  gausslemma2dlem4  15799  gausslemma2dlem5a  15800  lgseisenlem2  15806  lgsquadlem1  15812  2sqlem2  15850  mul2sq  15851  ushgredgedgloop  16085  clwwlkext2edg  16279  pw1map  16622  gsumgfsum1  16707  gsumgfsum  16710