Theorem 3eqtr3rd 2271

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 2264	. 2 |- ( ph -> B = C )
5	1, 4	eqtr3d 2264	1 |- ( ph -> D = C )

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  5907  fcof1o  5912  frecabcl  6543  nnaword  6655  nninfisol  7296  enomnilem  7301  fodju0  7310  enmkvlem  7324  enwomnilem  7332  pn0sr  7954  negeu  8333  add20  8617  2halves  9336  bcnn  10974  bcpasc  10983  wrdeqs1cat  11247  resqrexlemover  11516  fsumneg  11957  geolim  12017  geolim2  12018  mertensabs  12043  sincossq  12254  demoivre  12279  eirraplem  12283  gcdid  12502  gcdmultipled  12509  phiprmpw  12739  pythagtriplem12  12793  expnprm  12871  imasbas  13335  imasplusg  13336  imasmulr  13337  grpinvid1  13580  grpnpcan  13620  grplactcnv  13630  ghmgrp  13650  conjghm  13808  ringnegl  14009  ringnegr  14010  ringmneg2  14012  ring1  14017  rdivmuldivd  14102  lmodfopne  14284  lmodvsneg  14289  ioo2bl  15219  ptolemy  15492  coskpi  15516  logbgcd1irr  15635  logbgcd1irraplemap  15637  lgseisenlem3  15745  lgseisenlem4  15746  lgsquadlem1  15750  lgsquadlem2  15751