Theorem 3eqtrd 1503

Description: A deduction from three chained equalities.

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

Syntax hints:   -> wi 3   = wceq 953

This theorem is referenced by:  csbnestg 2026  csbopabg 2668  csbima12g 3397  resiima 3403  csbfv12g 3727  csboprg 3971  om1 4160  oe1 4162  oarec 4180  nneob 4239  ltexpq 5052  halfpq 5054  addsubt 5356  muladdt 5393  negsubdi2t 5430  nnncan1t 5439  mulsubt 5449  recextlem1 5655  muleqaddt 5669  div23t 5705  div12t 5707  divdivdivt 5741  conjmult 5753  nndivtrt 5907  uzindOLD 6156  uzrdgsuc 6241  seqz1 6479  seqzp1 6480  seq0p1 6483  seqzval2t 6485  mulexpt 6525  divexpt 6530  imret 6710  cjreimt 6763  cjreim2t 6764  cjdiv 6826  ser1absdiflem 6866  facp1t 6873  bcn0t 6901  bcnp11t 6903  fsum1 6943  fsump1 6944  fsumshft 6969  fsumconst 6976  binomlem1 7004  binomlem2 7005  binomlem6 7009  caucvg3a 7100  caucvg3lem 7102  isumnul 7138  fnsmntlem 7160  geoisumr 7178  efcltlem1 7246  ef0lem 7252  efaddlem5 7284  ef01tllem1 7325  abspef01tlub 7336  efi4pt 7377  resin4pt 7378  recos4pt 7379  efmivalt 7390  efeult 7391  absefit 7424  demoivre 7426  cnconst 7719  grpidinvlem1 7982  grpinvid2 8007  grpinvop 8015  grpinvdiv 8019  grppncan 8025  grpnpcan 8026  grppnpcan2 8027  ablmuldiv 8044  ablnncan 8049  ablmul 8068  ghsubgi 8075  vcz 8126  vcnegsubdi2 8131  vcoprne 8136  nvnegneg 8211  nvsubadd 8215  nvpncan2 8216  nvnncan 8223  nvdif 8232  nvpi 8233  nvabs 8240  nvge0 8241  nv1 8243  nvnd 8257  imsmetlem 8261  ipid 8297  ipcj 8301  lnocoi 8352  cnph 8409  ipasslem5 8425  ipasslem11 8431  ubthlem10 8469  minveclem28 8503  sincolem 8584  sinper 8609  cosper 8610  sinmpi 8613  cosmpi 8614  sinhalfpip 8616  sinhalfpim 8617  coshalfpim 8619  shftefif1olem 8661  shftefif1olemOLD 8662  effoi 8666  effoiOLD 8667  hvpncant 8829  hvaddsub4t 8866  his5t 8874  his2subt 8879  bcsALT 8967  norm1t 9042  hhssmetdval 9066  chocuni 9088  pjthlem7 9140  pjthlem8 9141  pjspansnt 9417  fh1t 9478  fh2t 9479  cm2jt 9480  5oalem2 9517  5oalem3 9518  5oalem5 9520  3oalem2 9525  pjv 9567  mayete3 9590  hoaddid1 9629  hosubid1t 9641  hoadddit 9646  honegsubdi2t 9654  hoaddsubt 9659  unoplint 9760  counopt 9761  hmoplint 9782  hmopcot 9863  nlelsh 9908  riesz3 9910  adjco 9947  branmfnt 9951  kbass2t 9962  kbass6t 9966  hmopidmpj 9991  pjsspos 10011  pjclem4 10037  pj3s 10045  strlem1 10087  stcltrlem1 10113  mdexch 10170  irredlem2 10226  ghomf1olem 10301  cayleylem2 10317  infi1 10347  moec 10357  2wsms 10474  1cat 10536  isfuna 10592

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1462

Copyright terms: Public domain