Theorem 3eqtrd 2233

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

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  tpeq123d  3715  diftpsn3  3764  oteq123d  3824  resiima  5028  fvun1  5630  fvmptd  5645  fmptpr  5757  caovlem2d  6120  offval  6147  ofvalg  6149  cnvf1olem  6291  nnm1  6592  updjudhcoinlf  7155  updjudhcoinrg  7156  caseinl  7166  caseinr  7167  omp1eomlem  7169  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  ltexnqq  7492  prarloclemarch  7502  ltrnqg  7504  nq02m  7549  prarloclemcalc  7586  mulnqprl  7652  mulnqpru  7653  ltexprlemloc  7691  addcanprleml  7698  recexprlem1ssu  7718  cauappcvgprlem1  7743  caucvgsrlemfv  7875  caucvgsrlemoffval  7880  recidpirqlemcalc  7941  axmulass  7957  axrnegex  7963  muladd11r  8199  addcan2  8224  addsub  8254  subsub2  8271  negsubdi2  8302  muladd  8427  mulsub  8444  cru  8646  mulreim  8648  recextlem1  8695  mulap0  8698  muleqadd  8712  divrecap  8732  div23ap  8735  div12ap  8738  divmulasscomap  8740  divcanap7  8765  conjmulap  8773  apmul1  8832  nndivtr  9049  subhalfhalf  9243  xp1d2m1eqxm1d2  9261  div4p1lem1div2  9262  qapne  9730  xnegneg  9925  rexsub  9945  xnegid  9951  fseq1p1m1  10186  nn0split  10228  nnsplit  10229  fzosplitsnm1  10302  fzosplitprm1  10327  ceilid  10424  flqdiv  10430  zmod10  10449  modqcyc  10468  modqaddabs  10471  mulqaddmodid  10473  modqadd2mod  10483  modqm1p1mod0  10484  modqmul12d  10487  modqadd12d  10489  modqmulmodr  10499  modqaddmulmod  10500  frecuzrdgsuc  10523  seqeq123d  10565  seqvalcd  10570  seq3f1olemqsumkj  10620  seq3f1oleml  10625  seqf1oglem2  10629  seq3id3  10633  seq3id  10634  seq3homo  10636  seq3z  10637  seqhomog  10639  exp1  10654  expnegap0  10656  expmulzap  10694  m1expeven  10695  expdivap  10699  binom3  10766  sqoddm1div8  10802  mulsubdivbinom2ap  10820  bcn1  10867  bcnp1n  10868  bcval5  10872  bcn2m1  10878  bcn2p1  10879  hashdifpr  10929  crim  11040  remullem  11053  remul2  11055  immul2  11062  ipcnval  11068  cjreim  11085  recvguniqlem  11176  resqrexlemover  11192  resqrexlemcalc1  11196  absid  11253  amgm2  11300  max0addsup  11401  minabs  11418  xrmaxrecl  11437  xrminadd  11457  fsumsplitf  11590  sumsnf  11591  fsump1i  11615  fsum2dlemstep  11616  fsumshftm  11627  fsummulc2  11630  modfsummodlemstep  11639  telfsumo  11648  fsumrelem  11653  hash2iun1dif1  11662  binomlem  11665  binom1dif  11669  arisum  11680  geo2sum  11696  geo2sum2  11697  cvgratz  11714  mertenslemi1  11717  clim2prod  11721  fprodeq0  11799  fprod2dlemstep  11804  fproddivap  11812  fproddivapf  11813  fprodmodd  11823  ef0lem  11842  eftlub  11872  efsep  11873  effsumlt  11874  tanval2ap  11895  efi4p  11899  resin4p  11900  recos4p  11901  efeul  11916  sinadd  11918  cosadd  11919  sinmul  11926  ef01bndlem  11938  cos12dec  11950  absef  11952  demoivreALT  11956  dvds2ln  12006  dvdseq  12030  opeo  12079  bezoutlemnewy  12188  nninfctlemfo  12232  eucalginv  12249  eucalglt  12250  eucalg  12252  lcmgcdlem  12270  lcm1  12274  divgcdcoprmex  12295  2sqpwodd  12369  zgcdsq  12394  qden1elz  12398  phiprmpw  12415  eulerthlem1  12420  eulerthlemrprm  12422  prmdiv  12428  hashgcdlem  12431  odzdvds  12439  vfermltl  12445  modprm0  12448  pythagtriplem12  12469  pcqmul  12497  pcaddlem  12533  pcadd  12534  pcadd2  12535  pcmpt  12537  pcmpt2  12538  mul4sqlem  12587  4sqlem11  12595  4sqlem17  12601  nninfdclemp1  12692  ressressg  12778  gsumsplit1r  13100  gsumprval  13101  mndinvmod  13147  mhmco  13192  gsumfzz  13197  grpinvid2  13255  grpasscan2  13266  grpinvssd  13279  grpinvadd  13280  grpsubid1  13287  grpsubadd  13290  grppncan  13293  mulg1  13335  mulgaddcomlem  13351  mulgdirlem  13359  mulgneg2  13362  mulgmodid  13367  nmzsubg  13416  qusinv  13442  qussub  13443  conjnmz  13485  ablsub2inv  13517  abladdsub4  13520  abladdsub  13521  ablpncan2  13522  ablpnpcan  13526  ablnncan  13527  invghm  13535  gsumfzconst  13547  gsumfzsnfd  13551  rngm2neg  13581  srgpcompp  13623  srgpcomppsc  13624  ringinvnzdiv  13682  ringm2neg  13687  dvr1  13770  dvrcan1  13772  dvrcan3  13773  rdivmuldivd  13776  lmodfopne  13958  sralemg  14070  gsumfzfsumlemm  14219  xmetxpbl  14828  ivthinclemuopn  14958  limcimolemlt  14984  cnplimcim  14987  limccnpcntop  14995  limccnp2lem  14996  dvexp  15031  dvmptcmulcn  15041  dvply1  15085  ef2kpi  15126  sinhalfpip  15140  sinhalfpim  15141  coshalfpim  15143  ptolemy  15144  tangtx  15158  rpabscxpbnd  15260  relogbexpap  15278  rplogbcxp  15283  rpcxplogb  15284  binom4  15299  wilthlem1  15300  0sgm  15305  mpodvdsmulf1o  15310  fsumdvdsmul  15311  sgmppw  15312  0sgmppw  15313  1sgm2ppw  15315  perfectlem1  15319  perfectlem2  15320  perfect  15321  lgsval2lem  15335  lgsval4  15345  lgsval4a  15347  lgsneg  15349  lgsneg1  15350  lgsdirprm  15359  lgsdir  15360  lgsne0  15363  lgsmulsqcoprm  15371  gausslemma2dlem1a  15383  gausslemma2dlem6  15392  gausslemma2d  15394  lgseisenlem3  15397  lgseisenlem4  15398  lgseisen  15399  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem1  15406  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2lgslem3d1  15425  2sqlem3  15442  peano4nninf  15737  trilpolemclim  15767  trilpolemeq1  15771  apdifflemf  15777