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  7473  enomnilem  7478  fodju0  7487  enmkvlem  7501  enwomnilem  7509  pn0sr  8138  negeu  8517  add20  8802  2halves  9534  lincmble  10406  bcnn  11195  bcpasc  11204  wrdeqs1cat  11492  resqrexlemover  11776  fsumneg  12218  geolim  12278  geolim2  12279  mertensabs  12304  sincossq  12515  demoivre  12540  eirraplem  12544  gcdid  12763  gcdmultipled  12770  phiprmpw  13000  pythagtriplem12  13054  expnprm  13132  ballotfilemrinv0  13276  imasbas  13628  imasplusg  13629  imasmulr  13630  grpinvid1  13857  grpnpcan  13897  grplactcnv  13907  ghmgrp  13921  conjghm  14079  ringnegl  14356  ringnegr  14357  ringmneg2  14359  ring1  14364  rdivmuldivd  14451  lmodfopne  14663  lmodvsneg  14668  ioo2bl  15652  ptolemy  15925  coskpi  15949  logbgcd1irr  16069  logbgcd1irraplemap  16071  birthdaylem2  16088  lgseisenlem3  16191  lgseisenlem4  16192  lgsquadlem1  16196  lgsquadlem2  16197