Theorem 3eqtr3rd 2219

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 2212	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
5	1, 4	eqtr3d 2212	1 ⊢ (𝜑 → 𝐷 = 𝐶)

Syntax hints:   → wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  fcofo  5787  fcof1o  5792  frecabcl  6402  nnaword  6514  nninfisol  7133  enomnilem  7138  fodju0  7147  enmkvlem  7161  enwomnilem  7169  pn0sr  7772  negeu  8150  add20  8433  2halves  9150  bcnn  10739  bcpasc  10748  resqrexlemover  11021  fsumneg  11461  geolim  11521  geolim2  11522  mertensabs  11547  sincossq  11758  demoivre  11782  eirraplem  11786  gcdid  11989  gcdmultipled  11996  phiprmpw  12224  pythagtriplem12  12277  expnprm  12353  imasbas  12733  imasplusg  12734  imasmulr  12735  grpinvid1  12929  grpnpcan  12967  grplactcnv  12977  ghmgrp  12987  ringnegl  13233  ringnegr  13234  ringmneg2  13236  ring1  13241  rdivmuldivd  13318  lmodfopne  13421  lmodvsneg  13426  lss0v  13521  ioo2bl  14128  ptolemy  14330  coskpi  14354  logbgcd1irr  14470  logbgcd1irraplemap  14472