Theorem 3eqtrd 2242

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

Syntax hints:   -> wi 4   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  tpeq123d  3725  diftpsn3  3774  oteq123d  3834  resiima  5041  fvun1  5647  fvmptd  5662  fmptpr  5778  caovlem2d  6141  offval  6168  ofvalg  6170  cnvf1olem  6312  nnm1  6613  updjudhcoinlf  7184  updjudhcoinrg  7185  caseinl  7195  caseinr  7196  omp1eomlem  7198  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  ltexnqq  7523  prarloclemarch  7533  ltrnqg  7535  nq02m  7580  prarloclemcalc  7617  mulnqprl  7683  mulnqpru  7684  ltexprlemloc  7722  addcanprleml  7729  recexprlem1ssu  7749  cauappcvgprlem1  7774  caucvgsrlemfv  7906  caucvgsrlemoffval  7911  recidpirqlemcalc  7972  axmulass  7988  axrnegex  7994  muladd11r  8230  addcan2  8255  addsub  8285  subsub2  8302  negsubdi2  8333  muladd  8458  mulsub  8475  cru  8677  mulreim  8679  recextlem1  8726  mulap0  8729  muleqadd  8743  divrecap  8763  div23ap  8766  div12ap  8769  divmulasscomap  8771  divcanap7  8796  conjmulap  8804  apmul1  8863  nndivtr  9080  subhalfhalf  9274  xp1d2m1eqxm1d2  9292  div4p1lem1div2  9293  qapne  9762  xnegneg  9957  rexsub  9977  xnegid  9983  fseq1p1m1  10218  nn0split  10260  nnsplit  10261  fzosplitsnm1  10340  fzosplitprm1  10365  ceilid  10462  flqdiv  10468  zmod10  10487  modqcyc  10506  modqaddabs  10509  mulqaddmodid  10511  modqadd2mod  10521  modqm1p1mod0  10522  modqmul12d  10525  modqadd12d  10527  modqmulmodr  10537  modqaddmulmod  10538  frecuzrdgsuc  10561  seqeq123d  10603  seqvalcd  10608  seq3f1olemqsumkj  10658  seq3f1oleml  10663  seqf1oglem2  10667  seq3id3  10671  seq3id  10672  seq3homo  10674  seq3z  10675  seqhomog  10677  exp1  10692  expnegap0  10694  expmulzap  10732  m1expeven  10733  expdivap  10737  binom3  10804  sqoddm1div8  10840  mulsubdivbinom2ap  10858  bcn1  10905  bcnp1n  10906  bcval5  10910  bcn2m1  10916  bcn2p1  10917  hashdifpr  10967  ccatlen  11054  ccats1val2  11095  lswccats1  11098  swrdlend  11114  ccatswrd  11126  pfxmpt  11134  pfxfv  11138  pfxfvlsw  11149  ccatpfx  11155  pfx1  11157  crim  11202  remullem  11215  remul2  11217  immul2  11224  ipcnval  11230  cjreim  11247  recvguniqlem  11338  resqrexlemover  11354  resqrexlemcalc1  11358  absid  11415  amgm2  11462  max0addsup  11563  minabs  11580  xrmaxrecl  11599  xrminadd  11619  fsumsplitf  11752  sumsnf  11753  fsump1i  11777  fsum2dlemstep  11778  fsumshftm  11789  fsummulc2  11792  modfsummodlemstep  11801  telfsumo  11810  fsumrelem  11815  hash2iun1dif1  11824  binomlem  11827  binom1dif  11831  arisum  11842  geo2sum  11858  geo2sum2  11859  cvgratz  11876  mertenslemi1  11879  clim2prod  11883  fprodeq0  11961  fprod2dlemstep  11966  fproddivap  11974  fproddivapf  11975  fprodmodd  11985  ef0lem  12004  eftlub  12034  efsep  12035  effsumlt  12036  tanval2ap  12057  efi4p  12061  resin4p  12062  recos4p  12063  efeul  12078  sinadd  12080  cosadd  12081  sinmul  12088  ef01bndlem  12100  cos12dec  12112  absef  12114  demoivreALT  12118  dvds2ln  12168  dvdseq  12192  opeo  12241  bezoutlemnewy  12350  nninfctlemfo  12394  eucalginv  12411  eucalglt  12412  eucalg  12414  lcmgcdlem  12432  lcm1  12436  divgcdcoprmex  12457  2sqpwodd  12531  zgcdsq  12556  qden1elz  12560  phiprmpw  12577  eulerthlem1  12582  eulerthlemrprm  12584  prmdiv  12590  hashgcdlem  12593  odzdvds  12601  vfermltl  12607  modprm0  12610  pythagtriplem12  12631  pcqmul  12659  pcaddlem  12695  pcadd  12696  pcadd2  12697  pcmpt  12699  pcmpt2  12700  mul4sqlem  12749  4sqlem11  12757  4sqlem17  12763  nninfdclemp1  12854  ressressg  12940  gsumsplit1r  13263  gsumprval  13264  mndinvmod  13310  mhmco  13355  gsumfzz  13360  grpinvid2  13418  grpasscan2  13429  grpinvssd  13442  grpinvadd  13443  grpsubid1  13450  grpsubadd  13453  grppncan  13456  mulg1  13498  mulgaddcomlem  13514  mulgdirlem  13522  mulgneg2  13525  mulgmodid  13530  nmzsubg  13579  qusinv  13605  qussub  13606  conjnmz  13648  ablsub2inv  13680  abladdsub4  13683  abladdsub  13684  ablpncan2  13685  ablpnpcan  13689  ablnncan  13690  invghm  13698  gsumfzconst  13710  gsumfzsnfd  13714  rngm2neg  13744  srgpcompp  13786  srgpcomppsc  13787  ringinvnzdiv  13845  ringm2neg  13850  dvr1  13933  dvrcan1  13935  dvrcan3  13936  rdivmuldivd  13939  lmodfopne  14121  sralemg  14233  gsumfzfsumlemm  14382  mplsubgfilemcl  14494  mplsubgfileminv  14495  xmetxpbl  15013  ivthinclemuopn  15143  limcimolemlt  15169  cnplimcim  15172  limccnpcntop  15180  limccnp2lem  15181  dvexp  15216  dvmptcmulcn  15226  dvply1  15270  ef2kpi  15311  sinhalfpip  15325  sinhalfpim  15326  coshalfpim  15328  ptolemy  15329  tangtx  15343  rpabscxpbnd  15445  relogbexpap  15463  rplogbcxp  15468  rpcxplogb  15469  binom4  15484  wilthlem1  15485  0sgm  15490  mpodvdsmulf1o  15495  fsumdvdsmul  15496  sgmppw  15497  0sgmppw  15498  1sgm2ppw  15500  perfectlem1  15504  perfectlem2  15505  perfect  15506  lgsval2lem  15520  lgsval4  15530  lgsval4a  15532  lgsneg  15534  lgsneg1  15535  lgsdirprm  15544  lgsdir  15545  lgsne0  15548  lgsmulsqcoprm  15556  gausslemma2dlem1a  15568  gausslemma2dlem6  15577  gausslemma2d  15579  lgseisenlem3  15582  lgseisenlem4  15583  lgseisen  15584  lgsquadlem1  15587  lgsquadlem2  15588  lgsquad2lem1  15591  2lgslem3a  15603  2lgslem3b  15604  2lgslem3c  15605  2lgslem3d  15606  2lgslem3d1  15610  2sqlem3  15627  structiedg0val  15670  peano4nninf  15980  trilpolemclim  16012  trilpolemeq1  16016  apdifflemf  16022