Theorem 3eqtrd 2117

Description: A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)

Hypotheses

Ref	Expression
3eqtrd.1	|- ( ph -> A = B )
3eqtrd.2	|- ( ph -> B = C )
3eqtrd.3	|- ( ph -> C = D )

Assertion

Ref	Expression
3eqtrd	|- ( ph -> A = D )

Proof of Theorem 3eqtrd

Step	Hyp	Ref	Expression
1		3eqtrd.1	. 2 |- ( ph -> A = B )
2		3eqtrd.2	. . 3 |- ( ph -> B = C )
3		3eqtrd.3	. . 3 |- ( ph -> C = D )
4	2, 3	eqtrd 2113	. 2 |- ( ph -> B = D )
5	1, 4	eqtrd 2113	1 |- ( ph -> A = D )

Syntax hints:   -> wi 4   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  tpeq123d  3484  diftpsn3  3527  oteq123d  3585  resiima  4703  fvun1  5260  fvmptd  5274  fmptpr  5376  caovlem2d  5713  offval  5739  fnofval  5741  cnvf1olem  5865  nnm1  6120  ltexnqq  6598  prarloclemarch  6608  ltrnqg  6610  nq02m  6655  prarloclemcalc  6692  mulnqprl  6758  mulnqpru  6759  ltexprlemloc  6797  addcanprleml  6804  recexprlem1ssu  6824  cauappcvgprlem1  6849  caucvgsrlemfv  6967  caucvgsrlemoffval  6972  recidpirqlemcalc  7025  axmulass  7039  axrnegex  7045  muladd11r  7264  addcan2  7289  addsub  7319  subsub2  7336  negsubdi2  7367  muladd  7488  mulsub  7505  cru  7702  mulreim  7704  recextlem1  7741  mulap0  7744  muleqadd  7758  divrecap  7776  div23ap  7779  div12ap  7782  divmulasscomap  7784  divcanap7  7809  conjmulap  7817  apmul1  7876  nndivtr  8080  xp1d2m1eqxm1d2  8283  div4p1lem1div2  8284  qapne  8724  xnegneg  8900  fseq1p1m1  9111  nn0split  9147  fzosplitsnm1  9218  fzosplitprm1  9243  ceilid  9317  flqdiv  9323  zmod10  9342  modqcyc  9361  modqaddabs  9364  mulqaddmodid  9366  modqadd2mod  9376  modqm1p1mod0  9377  modqmul12d  9380  modqadd12d  9382  modqmulmodr  9392  modqaddmulmod  9393  frecuzrdgsuc  9417  iseqid3s  9466  iseqid  9467  iseqhomo  9468  iseqz  9469  exp1  9482  expnegap0  9484  expmulzap  9522  m1expeven  9523  expdivap  9527  binom3  9590  sqoddm1div8  9625  bcn1  9685  bcnp1n  9686  ibcval5  9690  bcn2m1  9696  bcn2p1  9697  crim  9745  remullem  9758  remul2  9760  immul2  9767  ipcnval  9773  cjreim  9790  recvguniqlem  9880  resqrexlemover  9896  resqrexlemcalc1  9900  absid  9957  amgm2  10004  max0addsup  10105  dvds2ln  10228  dvdseq  10248  opeo  10297  bezoutlemnewy  10385  eucalginv  10438  eucalglt  10439  eucialg  10441  lcmgcdlem  10459  lcm1  10463  divgcdcoprmex  10484  2sqpwodd  10554