Theorem 3eqtr3rd 2247

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

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  fcofo  5853  fcof1o  5858  frecabcl  6485  nnaword  6597  nninfisol  7235  enomnilem  7240  fodju0  7249  enmkvlem  7263  enwomnilem  7271  pn0sr  7884  negeu  8263  add20  8547  2halves  9266  bcnn  10902  bcpasc  10911  resqrexlemover  11321  fsumneg  11762  geolim  11822  geolim2  11823  mertensabs  11848  sincossq  12059  demoivre  12084  eirraplem  12088  gcdid  12307  gcdmultipled  12314  phiprmpw  12544  pythagtriplem12  12598  expnprm  12676  imasbas  13139  imasplusg  13140  imasmulr  13141  grpinvid1  13384  grpnpcan  13424  grplactcnv  13434  ghmgrp  13454  conjghm  13612  ringnegl  13813  ringnegr  13814  ringmneg2  13816  ring1  13821  rdivmuldivd  13906  lmodfopne  14088  lmodvsneg  14093  ioo2bl  15023  ptolemy  15296  coskpi  15320  logbgcd1irr  15439  logbgcd1irraplemap  15441  lgseisenlem3  15549  lgseisenlem4  15550  lgsquadlem1  15554  lgsquadlem2  15555