Theorem 3eqtr3rd 2238

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

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  fcofo  5834  fcof1o  5839  frecabcl  6466  nnaword  6578  nninfisol  7208  enomnilem  7213  fodju0  7222  enmkvlem  7236  enwomnilem  7244  pn0sr  7855  negeu  8234  add20  8518  2halves  9237  bcnn  10866  bcpasc  10875  resqrexlemover  11192  fsumneg  11633  geolim  11693  geolim2  11694  mertensabs  11719  sincossq  11930  demoivre  11955  eirraplem  11959  gcdid  12178  gcdmultipled  12185  phiprmpw  12415  pythagtriplem12  12469  expnprm  12547  imasbas  13009  imasplusg  13010  imasmulr  13011  grpinvid1  13254  grpnpcan  13294  grplactcnv  13304  ghmgrp  13324  conjghm  13482  ringnegl  13683  ringnegr  13684  ringmneg2  13686  ring1  13691  rdivmuldivd  13776  lmodfopne  13958  lmodvsneg  13963  ioo2bl  14871  ptolemy  15144  coskpi  15168  logbgcd1irr  15287  logbgcd1irraplemap  15289  lgseisenlem3  15397  lgseisenlem4  15398  lgsquadlem1  15402  lgsquadlem2  15403