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  8518  add20  8803  2halves  9538  lincmble  10416  bcnn  11209  bcpasc  11218  wrdeqs1cat  11506  resqrexlemover  11790  fsumneg  12234  geolim  12294  geolim2  12295  mertensabs  12320  sincossq  12531  demoivre  12556  eirraplem  12560  gcdid  12779  gcdmultipled  12786  phiprmpw  13020  pythagtriplem12  13074  expnprm  13152  ballotfilemrinv0  13325  imasbas  13677  imasplusg  13678  imasmulr  13679  grpinvid1  13906  grpnpcan  13946  grplactcnv  13956  ghmgrp  13970  conjghm  14128  ringnegl  14405  ringnegr  14406  ringmneg2  14408  ring1  14413  rdivmuldivd  14500  lmodfopne  14712  lmodvsneg  14717  ioo2bl  15701  ptolemy  15975  coskpi  15999  logbgcd1irr  16122  logbgcd1irraplemap  16124  birthdaylem2  16145  bclbnd  16205  lgseisenlem3  16289  lgseisenlem4  16290  lgsquadlem1  16294  lgsquadlem2  16295