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  5901  fcof1o  5906  frecabcl  6535  nnaword  6647  nninfisol  7288  enomnilem  7293  fodju0  7302  enmkvlem  7316  enwomnilem  7324  pn0sr  7946  negeu  8325  add20  8609  2halves  9328  bcnn  10966  bcpasc  10975  wrdeqs1cat  11238  resqrexlemover  11507  fsumneg  11948  geolim  12008  geolim2  12009  mertensabs  12034  sincossq  12245  demoivre  12270  eirraplem  12274  gcdid  12493  gcdmultipled  12500  phiprmpw  12730  pythagtriplem12  12784  expnprm  12862  imasbas  13326  imasplusg  13327  imasmulr  13328  grpinvid1  13571  grpnpcan  13611  grplactcnv  13621  ghmgrp  13641  conjghm  13799  ringnegl  14000  ringnegr  14001  ringmneg2  14003  ring1  14008  rdivmuldivd  14093  lmodfopne  14275  lmodvsneg  14280  ioo2bl  15210  ptolemy  15483  coskpi  15507  logbgcd1irr  15626  logbgcd1irraplemap  15628  lgseisenlem3  15736  lgseisenlem4  15737  lgsquadlem1  15741  lgsquadlem2  15742