Theorem 3eqtr3rd 2248

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  fcofo  5863  fcof1o  5868  frecabcl  6495  nnaword  6607  nninfisol  7247  enomnilem  7252  fodju0  7261  enmkvlem  7275  enwomnilem  7283  pn0sr  7897  negeu  8276  add20  8560  2halves  9279  bcnn  10915  bcpasc  10924  resqrexlemover  11371  fsumneg  11812  geolim  11872  geolim2  11873  mertensabs  11898  sincossq  12109  demoivre  12134  eirraplem  12138  gcdid  12357  gcdmultipled  12364  phiprmpw  12594  pythagtriplem12  12648  expnprm  12726  imasbas  13189  imasplusg  13190  imasmulr  13191  grpinvid1  13434  grpnpcan  13474  grplactcnv  13484  ghmgrp  13504  conjghm  13662  ringnegl  13863  ringnegr  13864  ringmneg2  13866  ring1  13871  rdivmuldivd  13956  lmodfopne  14138  lmodvsneg  14143  ioo2bl  15073  ptolemy  15346  coskpi  15370  logbgcd1irr  15489  logbgcd1irraplemap  15491  lgseisenlem3  15599  lgseisenlem4  15600  lgsquadlem1  15604  lgsquadlem2  15605