Theorem 3eqtr3rd 2271

Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)

Hypotheses

Ref	Expression
3eqtr3d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)
3eqtr3d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3eqtr3rd	⊢ (𝜑 → 𝐷 = 𝐶)

Proof of Theorem 3eqtr3rd

Step	Hyp	Ref	Expression
1		3eqtr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
2		3eqtr3d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3		3eqtr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
4	2, 3	eqtr3d 2264	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
5	1, 4	eqtr3d 2264	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:  fcofo  5917  fcof1o  5922  frecabcl  6556  nnaword  6670  nninfisol  7316  enomnilem  7321  fodju0  7330  enmkvlem  7344  enwomnilem  7352  pn0sr  7974  negeu  8353  add20  8637  2halves  9356  bcnn  10996  bcpasc  11005  wrdeqs1cat  11273  resqrexlemover  11542  fsumneg  11983  geolim  12043  geolim2  12044  mertensabs  12069  sincossq  12280  demoivre  12305  eirraplem  12309  gcdid  12528  gcdmultipled  12535  phiprmpw  12765  pythagtriplem12  12819  expnprm  12897  imasbas  13361  imasplusg  13362  imasmulr  13363  grpinvid1  13606  grpnpcan  13646  grplactcnv  13656  ghmgrp  13676  conjghm  13834  ringnegl  14035  ringnegr  14036  ringmneg2  14038  ring1  14043  rdivmuldivd  14129  lmodfopne  14311  lmodvsneg  14316  ioo2bl  15246  ptolemy  15519  coskpi  15543  logbgcd1irr  15662  logbgcd1irraplemap  15664  lgseisenlem3  15772  lgseisenlem4  15773  lgsquadlem1  15777  lgsquadlem2  15778