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  5993  fcof1o  5998  frecabcl  6675  nnaword  6789  nninfisol  7479  enomnilem  7484  fodju0  7493  enmkvlem  7507  enwomnilem  7515  pn0sr  8144  negeu  8524  add20  8809  2halves  9545  lincmble  10422  bcnn  11216  bcpasc  11225  wrdeqs1cat  11513  resqrexlemover  11797  fsumneg  12242  geolim  12302  geolim2  12303  mertensabs  12328  sincossq  12539  demoivre  12564  eirraplem  12568  gcdid  12787  gcdmultipled  12794  phiprmpw  13028  pythagtriplem12  13082  expnprm  13160  ballotfilemrinv0  13333  imasbas  13686  imasplusg  13687  imasmulr  13688  grpinvid1  13915  grpnpcan  13955  grplactcnv  13965  ghmgrp  13979  conjghm  14137  ringnegl  14462  ringnegr  14463  ringmneg2  14465  ring1  14470  rdivmuldivd  14559  lmodfopne  14771  lmodvsneg  14776  ioo2bl  15794  ptolemy  16068  coskpi  16092  logbgcd1irr  16220  logbgcd1irraplemap  16222  birthdaylem2  16243  bclbnd  16324  lgseisenlem3  16413  lgseisenlem4  16414  lgsquadlem1  16418  lgsquadlem2  16419