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  3714  diftpsn3  3763  oteq123d  3823  resiima  5027  fvun1  5627  fvmptd  5642  fmptpr  5754  caovlem2d  6116  offval  6143  ofvalg  6145  cnvf1olem  6282  nnm1  6583  updjudhcoinlf  7146  updjudhcoinrg  7147  caseinl  7157  caseinr  7158  omp1eomlem  7160  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  ltexnqq  7475  prarloclemarch  7485  ltrnqg  7487  nq02m  7532  prarloclemcalc  7569  mulnqprl  7635  mulnqpru  7636  ltexprlemloc  7674  addcanprleml  7681  recexprlem1ssu  7701  cauappcvgprlem1  7726  caucvgsrlemfv  7858  caucvgsrlemoffval  7863  recidpirqlemcalc  7924  axmulass  7940  axrnegex  7946  muladd11r  8182  addcan2  8207  addsub  8237  subsub2  8254  negsubdi2  8285  muladd  8410  mulsub  8427  cru  8629  mulreim  8631  recextlem1  8678  mulap0  8681  muleqadd  8695  divrecap  8715  div23ap  8718  div12ap  8721  divmulasscomap  8723  divcanap7  8748  conjmulap  8756  apmul1  8815  nndivtr  9032  subhalfhalf  9226  xp1d2m1eqxm1d2  9244  div4p1lem1div2  9245  qapne  9713  xnegneg  9908  rexsub  9928  xnegid  9934  fseq1p1m1  10169  nn0split  10211  nnsplit  10212  fzosplitsnm1  10285  fzosplitprm1  10310  ceilid  10407  flqdiv  10413  zmod10  10432  modqcyc  10451  modqaddabs  10454  mulqaddmodid  10456  modqadd2mod  10466  modqm1p1mod0  10467  modqmul12d  10470  modqadd12d  10472  modqmulmodr  10482  modqaddmulmod  10483  frecuzrdgsuc  10506  seqeq123d  10548  seqvalcd  10553  seq3f1olemqsumkj  10603  seq3f1oleml  10608  seqf1oglem2  10612  seq3id3  10616  seq3id  10617  seq3homo  10619  seq3z  10620  seqhomog  10622  exp1  10637  expnegap0  10639  expmulzap  10677  m1expeven  10678  expdivap  10682  binom3  10749  sqoddm1div8  10785  mulsubdivbinom2ap  10803  bcn1  10850  bcnp1n  10851  bcval5  10855  bcn2m1  10861  bcn2p1  10862  hashdifpr  10912  crim  11023  remullem  11036  remul2  11038  immul2  11045  ipcnval  11051  cjreim  11068  recvguniqlem  11159  resqrexlemover  11175  resqrexlemcalc1  11179  absid  11236  amgm2  11283  max0addsup  11384  minabs  11401  xrmaxrecl  11420  xrminadd  11440  fsumsplitf  11573  sumsnf  11574  fsump1i  11598  fsum2dlemstep  11599  fsumshftm  11610  fsummulc2  11613  modfsummodlemstep  11622  telfsumo  11631  fsumrelem  11636  hash2iun1dif1  11645  binomlem  11648  binom1dif  11652  arisum  11663  geo2sum  11679  geo2sum2  11680  cvgratz  11697  mertenslemi1  11700  clim2prod  11704  fprodeq0  11782  fprod2dlemstep  11787  fproddivap  11795  fproddivapf  11796  fprodmodd  11806  ef0lem  11825  eftlub  11855  efsep  11856  effsumlt  11857  tanval2ap  11878  efi4p  11882  resin4p  11883  recos4p  11884  efeul  11899  sinadd  11901  cosadd  11902  sinmul  11909  ef01bndlem  11921  cos12dec  11933  absef  11935  demoivreALT  11939  dvds2ln  11989  dvdseq  12013  opeo  12062  bezoutlemnewy  12163  nninfctlemfo  12207  eucalginv  12224  eucalglt  12225  eucalg  12227  lcmgcdlem  12245  lcm1  12249  divgcdcoprmex  12270  2sqpwodd  12344  zgcdsq  12369  qden1elz  12373  phiprmpw  12390  eulerthlem1  12395  eulerthlemrprm  12397  prmdiv  12403  hashgcdlem  12406  odzdvds  12414  vfermltl  12420  modprm0  12423  pythagtriplem12  12444  pcqmul  12472  pcaddlem  12508  pcadd  12509  pcadd2  12510  pcmpt  12512  pcmpt2  12513  mul4sqlem  12562  4sqlem11  12570  4sqlem17  12576  nninfdclemp1  12667  ressressg  12753  gsumsplit1r  13041  gsumprval  13042  mndinvmod  13086  mhmco  13122  gsumfzz  13127  grpinvid2  13185  grpasscan2  13196  grpinvssd  13209  grpinvadd  13210  grpsubid1  13217  grpsubadd  13220  grppncan  13223  mulg1  13259  mulgaddcomlem  13275  mulgdirlem  13283  mulgneg2  13286  mulgmodid  13291  nmzsubg  13340  qusinv  13366  qussub  13367  conjnmz  13409  ablsub2inv  13441  abladdsub4  13444  abladdsub  13445  ablpncan2  13446  ablpnpcan  13450  ablnncan  13451  invghm  13459  gsumfzconst  13471  gsumfzsnfd  13475  rngm2neg  13505  srgpcompp  13547  srgpcomppsc  13548  ringinvnzdiv  13606  ringm2neg  13611  dvr1  13694  dvrcan1  13696  dvrcan3  13697  rdivmuldivd  13700  lmodfopne  13882  sralemg  13994  gsumfzfsumlemm  14143  xmetxpbl  14744  ivthinclemuopn  14874  limcimolemlt  14900  cnplimcim  14903  limccnpcntop  14911  limccnp2lem  14912  dvexp  14947  dvmptcmulcn  14957  dvply1  15001  ef2kpi  15042  sinhalfpip  15056  sinhalfpim  15057  coshalfpim  15059  ptolemy  15060  tangtx  15074  rpabscxpbnd  15176  relogbexpap  15194  rplogbcxp  15199  rpcxplogb  15200  binom4  15215  wilthlem1  15216  0sgm  15221  mpodvdsmulf1o  15226  fsumdvdsmul  15227  sgmppw  15228  0sgmppw  15229  1sgm2ppw  15231  perfectlem1  15235  perfectlem2  15236  perfect  15237  lgsval2lem  15251  lgsval4  15261  lgsval4a  15263  lgsneg  15265  lgsneg1  15266  lgsdirprm  15275  lgsdir  15276  lgsne0  15279  lgsmulsqcoprm  15287  gausslemma2dlem1a  15299  gausslemma2dlem6  15308  gausslemma2d  15310  lgseisenlem3  15313  lgseisenlem4  15314  lgseisen  15315  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem1  15322  2lgslem3a  15334  2lgslem3b  15335  2lgslem3c  15336  2lgslem3d  15337  2lgslem3d1  15341  2sqlem3  15358  peano4nninf  15650  trilpolemclim  15680  trilpolemeq1  15684  apdifflemf  15690