Theorem 3eqtr3rd 2280

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  fcofo  5990  fcof1o  5995  frecabcl  6670  nnaword  6784  nninfisol  7474  enomnilem  7479  fodju0  7488  enmkvlem  7502  enwomnilem  7510  pn0sr  8139  negeu  8519  add20  8804  2halves  9539  lincmble  10417  bcnn  11211  bcpasc  11220  wrdeqs1cat  11508  resqrexlemover  11792  fsumneg  12237  geolim  12297  geolim2  12298  mertensabs  12323  sincossq  12534  demoivre  12559  eirraplem  12563  gcdid  12782  gcdmultipled  12789  phiprmpw  13023  pythagtriplem12  13077  expnprm  13155  ballotfilemrinv0  13328  imasbas  13681  imasplusg  13682  imasmulr  13683  grpinvid1  13910  grpnpcan  13950  grplactcnv  13960  ghmgrp  13974  conjghm  14132  ringnegl  14440  ringnegr  14441  ringmneg2  14443  ring1  14448  rdivmuldivd  14535  lmodfopne  14747  lmodvsneg  14752  ioo2bl  15743  ptolemy  16017  coskpi  16041  logbgcd1irr  16164  logbgcd1irraplemap  16166  birthdaylem2  16187  bclbnd  16268  lgseisenlem3  16357  lgseisenlem4  16358  lgsquadlem1  16362  lgsquadlem2  16363