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  5831  fcof1o  5836  frecabcl  6457  nnaword  6569  nninfisol  7199  enomnilem  7204  fodju0  7213  enmkvlem  7227  enwomnilem  7235  pn0sr  7838  negeu  8217  add20  8501  2halves  9220  bcnn  10849  bcpasc  10858  resqrexlemover  11175  fsumneg  11616  geolim  11676  geolim2  11677  mertensabs  11702  sincossq  11913  demoivre  11938  eirraplem  11942  gcdid  12153  gcdmultipled  12160  phiprmpw  12390  pythagtriplem12  12444  expnprm  12522  imasbas  12950  imasplusg  12951  imasmulr  12952  grpinvid1  13184  grpnpcan  13224  grplactcnv  13234  ghmgrp  13248  conjghm  13406  ringnegl  13607  ringnegr  13608  ringmneg2  13610  ring1  13615  rdivmuldivd  13700  lmodfopne  13882  lmodvsneg  13887  ioo2bl  14787  ptolemy  15060  coskpi  15084  logbgcd1irr  15203  logbgcd1irraplemap  15205  lgseisenlem3  15313  lgseisenlem4  15314  lgsquadlem1  15318  lgsquadlem2  15319