Theorem 3eqtrd 2176

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

Syntax hints:   -> wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  tpeq123d  3615  diftpsn3  3661  oteq123d  3720  resiima  4897  fvun1  5487  fvmptd  5502  fmptpr  5612  caovlem2d  5963  offval  5989  ofvalg  5991  cnvf1olem  6121  nnm1  6420  updjudhcoinlf  6965  updjudhcoinrg  6966  caseinl  6976  caseinr  6977  omp1eomlem  6979  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  ltexnqq  7216  prarloclemarch  7226  ltrnqg  7228  nq02m  7273  prarloclemcalc  7310  mulnqprl  7376  mulnqpru  7377  ltexprlemloc  7415  addcanprleml  7422  recexprlem1ssu  7442  cauappcvgprlem1  7467  caucvgsrlemfv  7599  caucvgsrlemoffval  7604  recidpirqlemcalc  7665  axmulass  7681  axrnegex  7687  muladd11r  7918  addcan2  7943  addsub  7973  subsub2  7990  negsubdi2  8021  muladd  8146  mulsub  8163  cru  8364  mulreim  8366  recextlem1  8412  mulap0  8415  muleqadd  8429  divrecap  8448  div23ap  8451  div12ap  8454  divmulasscomap  8456  divcanap7  8481  conjmulap  8489  apmul1  8548  nndivtr  8762  xp1d2m1eqxm1d2  8972  div4p1lem1div2  8973  qapne  9431  xnegneg  9616  rexsub  9636  xnegid  9642  fseq1p1m1  9874  nn0split  9913  nnsplit  9914  fzosplitsnm1  9986  fzosplitprm1  10011  ceilid  10088  flqdiv  10094  zmod10  10113  modqcyc  10132  modqaddabs  10135  mulqaddmodid  10137  modqadd2mod  10147  modqm1p1mod0  10148  modqmul12d  10151  modqadd12d  10153  modqmulmodr  10163  modqaddmulmod  10164  frecuzrdgsuc  10187  seqeq123d  10227  seqvalcd  10232  seq3f1olemqsumkj  10271  seq3f1oleml  10276  seq3id3  10280  seq3id  10281  seq3homo  10283  seq3z  10284  exp1  10299  expnegap0  10301  expmulzap  10339  m1expeven  10340  expdivap  10344  binom3  10409  sqoddm1div8  10444  bcn1  10504  bcnp1n  10505  bcval5  10509  bcn2m1  10515  bcn2p1  10516  hashdifpr  10566  crim  10630  remullem  10643  remul2  10645  immul2  10652  ipcnval  10658  cjreim  10675  recvguniqlem  10766  resqrexlemover  10782  resqrexlemcalc1  10786  absid  10843  amgm2  10890  max0addsup  10991  minabs  11007  xrmaxrecl  11024  xrminadd  11044  fsumsplitf  11177  sumsnf  11178  fsump1i  11202  fsum2dlemstep  11203  fsumshftm  11214  fsummulc2  11217  modfsummodlemstep  11226  telfsumo  11235  fsumrelem  11240  hash2iun1dif1  11249  binomlem  11252  binom1dif  11256  arisum  11267  geo2sum  11283  geo2sum2  11284  cvgratz  11301  mertenslemi1  11304  clim2prod  11308  ef0lem  11366  eftlub  11396  efsep  11397  effsumlt  11398  tanval2ap  11420  efi4p  11424  resin4p  11425  recos4p  11426  efeul  11441  sinadd  11443  cosadd  11444  sinmul  11451  ef01bndlem  11463  cos12dec  11474  absef  11476  demoivreALT  11480  dvds2ln  11526  dvdseq  11546  opeo  11594  bezoutlemnewy  11684  eucalginv  11737  eucalglt  11738  eucalg  11740  lcmgcdlem  11758  lcm1  11762  divgcdcoprmex  11783  2sqpwodd  11854  zgcdsq  11879  qden1elz  11883  phiprmpw  11898  hashgcdlem  11903  xmetxpbl  12677  ivthinclemuopn  12785  limcimolemlt  12802  cnplimcim  12805  limccnpcntop  12813  limccnp2lem  12814  dvexp  12844  dvmptcmulcn  12852  ef2kpi  12887  sinhalfpip  12901  sinhalfpim  12902  coshalfpim  12904  ptolemy  12905  tangtx  12919  peano4nninf  13200  trilpolemclim  13229  trilpolemeq1  13233