Theorem 3eqtr3rd 2273

Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)

Hypotheses

Ref	Expression
3eqtr3d.1	|- ( ph -> A = B )
3eqtr3d.2	|- ( ph -> A = C )
3eqtr3d.3	|- ( ph -> B = D )

Assertion

Ref	Expression
3eqtr3rd	|- ( ph -> D = C )

Proof of Theorem 3eqtr3rd

Step	Hyp	Ref	Expression
1		3eqtr3d.3	. 2 |- ( ph -> B = D )
2		3eqtr3d.1	. . 3 |- ( ph -> A = B )
3		3eqtr3d.2	. . 3 |- ( ph -> A = C )
4	2, 3	eqtr3d 2266	. 2 |- ( ph -> B = C )
5	1, 4	eqtr3d 2266	1 |- ( ph -> D = C )

Syntax hints:   -> wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  fcofo  5924  fcof1o  5929  frecabcl  6564  nnaword  6678  nninfisol  7331  enomnilem  7336  fodju0  7345  enmkvlem  7359  enwomnilem  7367  pn0sr  7990  negeu  8369  add20  8653  2halves  9372  bcnn  11018  bcpasc  11027  wrdeqs1cat  11300  resqrexlemover  11570  fsumneg  12011  geolim  12071  geolim2  12072  mertensabs  12097  sincossq  12308  demoivre  12333  eirraplem  12337  gcdid  12556  gcdmultipled  12563  phiprmpw  12793  pythagtriplem12  12847  expnprm  12925  imasbas  13389  imasplusg  13390  imasmulr  13391  grpinvid1  13634  grpnpcan  13674  grplactcnv  13684  ghmgrp  13704  conjghm  13862  ringnegl  14063  ringnegr  14064  ringmneg2  14066  ring1  14071  rdivmuldivd  14157  lmodfopne  14339  lmodvsneg  14344  ioo2bl  15274  ptolemy  15547  coskpi  15571  logbgcd1irr  15690  logbgcd1irraplemap  15692  lgseisenlem3  15800  lgseisenlem4  15801  lgsquadlem1  15805  lgsquadlem2  15806