Theorem 3eqtr3rd 2274

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  fcofo  5957  fcof1o  5962  frecabcl  6630  nnaword  6744  nninfisol  7424  enomnilem  7429  fodju0  7438  enmkvlem  7452  enwomnilem  7460  pn0sr  8086  negeu  8464  add20  8748  2halves  9467  lincmble  10337  bcnn  11119  bcpasc  11128  wrdeqs1cat  11412  resqrexlemover  11695  fsumneg  12137  geolim  12197  geolim2  12198  mertensabs  12223  sincossq  12434  demoivre  12459  eirraplem  12463  gcdid  12682  gcdmultipled  12689  phiprmpw  12919  pythagtriplem12  12973  expnprm  13051  imasbas  13520  imasplusg  13521  imasmulr  13522  grpinvid1  13765  grpnpcan  13805  grplactcnv  13815  ghmgrp  13835  conjghm  13993  ringnegl  14195  ringnegr  14196  ringmneg2  14198  ring1  14203  rdivmuldivd  14289  lmodfopne  14474  lmodvsneg  14479  ioo2bl  15416  ptolemy  15689  coskpi  15713  logbgcd1irr  15832  logbgcd1irraplemap  15834  lgseisenlem3  15945  lgseisenlem4  15946  lgsquadlem1  15950  lgsquadlem2  15951