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 )

Syntax hints:   -> wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  fcofo  5980  fcof1o  5985  frecabcl  6660  nnaword  6774  nninfisol  7463  enomnilem  7468  fodju0  7477  enmkvlem  7491  enwomnilem  7499  pn0sr  8128  negeu  8507  add20  8792  2halves  9513  lincmble  10385  bcnn  11173  bcpasc  11182  wrdeqs1cat  11470  resqrexlemover  11754  fsumneg  12196  geolim  12256  geolim2  12257  mertensabs  12282  sincossq  12493  demoivre  12518  eirraplem  12522  gcdid  12741  gcdmultipled  12748  phiprmpw  12978  pythagtriplem12  13032  expnprm  13110  ballotfilemrinv0  13254  imasbas  13605  imasplusg  13606  imasmulr  13607  grpinvid1  13834  grpnpcan  13874  grplactcnv  13884  ghmgrp  13898  conjghm  14056  ringnegl  14329  ringnegr  14330  ringmneg2  14332  ring1  14337  rdivmuldivd  14424  lmodfopne  14635  lmodvsneg  14640  ioo2bl  15575  ptolemy  15848  coskpi  15872  logbgcd1irr  15992  logbgcd1irraplemap  15994  lgseisenlem3  16105  lgseisenlem4  16106  lgsquadlem1  16110  lgsquadlem2  16111