Theorem 3eqtrd 2149

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 2145	. 2 |- ( ph -> B = D )
5	1, 4	eqtrd 2145	1 |- ( ph -> A = D )

Syntax hints:   -> wi 4   = wceq 1312

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-4 1468  ax-17 1487  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-cleq 2106

This theorem is referenced by:  tpeq123d  3579  diftpsn3  3625  oteq123d  3684  resiima  4853  fvun1  5439  fvmptd  5454  fmptpr  5564  caovlem2d  5915  offval  5941  ofvalg  5943  cnvf1olem  6073  nnm1  6372  updjudhcoinlf  6915  updjudhcoinrg  6916  caseinl  6926  caseinr  6927  omp1eomlem  6929  exmidfodomrlemr  7003  exmidfodomrlemrALT  7004  ltexnqq  7158  prarloclemarch  7168  ltrnqg  7170  nq02m  7215  prarloclemcalc  7252  mulnqprl  7318  mulnqpru  7319  ltexprlemloc  7357  addcanprleml  7364  recexprlem1ssu  7384  cauappcvgprlem1  7409  caucvgsrlemfv  7527  caucvgsrlemoffval  7532  recidpirqlemcalc  7586  axmulass  7602  axrnegex  7608  muladd11r  7835  addcan2  7860  addsub  7890  subsub2  7907  negsubdi2  7938  muladd  8059  mulsub  8076  cru  8276  mulreim  8278  recextlem1  8319  mulap0  8322  muleqadd  8336  divrecap  8355  div23ap  8358  div12ap  8361  divmulasscomap  8363  divcanap7  8388  conjmulap  8396  apmul1  8455  nndivtr  8666  xp1d2m1eqxm1d2  8870  div4p1lem1div2  8871  qapne  9327  xnegneg  9503  rexsub  9523  xnegid  9529  fseq1p1m1  9761  nn0split  9800  nnsplit  9801  fzosplitsnm1  9873  fzosplitprm1  9898  ceilid  9975  flqdiv  9981  zmod10  10000  modqcyc  10019  modqaddabs  10022  mulqaddmodid  10024  modqadd2mod  10034  modqm1p1mod0  10035  modqmul12d  10038  modqadd12d  10040  modqmulmodr  10050  modqaddmulmod  10051  frecuzrdgsuc  10074  seqeq123d  10114  seqvalcd  10119  seq3f1olemqsumkj  10158  seq3f1oleml  10163  seq3id3  10167  seq3id  10168  seq3homo  10170  seq3z  10171  exp1  10186  expnegap0  10188  expmulzap  10226  m1expeven  10227  expdivap  10231  binom3  10296  sqoddm1div8  10331  bcn1  10391  bcnp1n  10392  bcval5  10396  bcn2m1  10402  bcn2p1  10403  hashdifpr  10453  crim  10517  remullem  10530  remul2  10532  immul2  10539  ipcnval  10545  cjreim  10562  recvguniqlem  10652  resqrexlemover  10668  resqrexlemcalc1  10672  absid  10729  amgm2  10776  max0addsup  10877  minabs  10893  xrmaxrecl  10910  xrminadd  10930  fsumsplitf  11063  sumsnf  11064  fsump1i  11088  fsum2dlemstep  11089  fsumshftm  11100  fsummulc2  11103  modfsummodlemstep  11112  telfsumo  11121  fsumrelem  11126  hash2iun1dif1  11135  binomlem  11138  binom1dif  11142  arisum  11153  geo2sum  11169  geo2sum2  11170  cvgratz  11187  mertenslemi1  11190  ef0lem  11211  eftlub  11241  efsep  11242  effsumlt  11243  tanval2ap  11265  efi4p  11269  resin4p  11270  recos4p  11271  efeul  11286  sinadd  11288  cosadd  11289  sinmul  11296  ef01bndlem  11308  absef  11320  demoivreALT  11324  dvds2ln  11368  dvdseq  11388  opeo  11436  bezoutlemnewy  11524  eucalginv  11577  eucalglt  11578  eucalg  11580  lcmgcdlem  11598  lcm1  11602  divgcdcoprmex  11623  2sqpwodd  11693  zgcdsq  11718  qden1elz  11722  phiprmpw  11737  hashgcdlem  11742  xmetxpbl  12491  limcimolemlt  12583  cnplimcim  12586  limccnpcntop  12594  limccnp2lem  12595  peano4nninf  12881  trilpolemclim  12910  trilpolemeq1  12914