Theorem 3eqtrd 1511

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

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  csbnestg 2036  csbopabg 2678  csbima12g 3413  resiima 3419  csbfv12g 3742  csboprg 3986  om1 4176  oe1 4178  oarec 4196  nneob 4255  ltexpq 5080  halfpq 5082  addsubt 5384  muladdt 5421  negsubdi2t 5458  nnncan1t 5467  mulsubt 5477  recextlem1 5682  muleqaddt 5700  div23t 5742  div12t 5744  divdivdivt 5785  conjmult 5797  nndivtrt 5960  uzindOLD 6208  uzrdgsuc 6304  seqz1 6547  seqzp1 6548  seq0p1 6551  seqzval2t 6553  mulexpt 6594  divexpt 6599  imret 6773  mulretOLD 6777  cjreimt 6828  cjreim2t 6829  cjdiv 6888  ser1absdiflem 6929  facp1t 6936  bcn0t 6963  bcnp11t 6965  fsum1 7005  fsump1 7006  fsumshft 7031  fsumconst 7038  binomlem1 7066  binomlem2 7067  binomlem6 7071  isumnul 7203  fnsmntlem 7225  geoisumr 7243  efcltlem1 7304  ef0lem 7310  efaddlem5 7342  ef01tllem1 7383  abspef01tlub 7395  efi4pt 7435  resin4pt 7436  recos4pt 7437  efmivalt 7448  efeult 7449  absefit 7482  demoivre 7484  cnconst 7780  grpidinvlem1 8048  grpinvid2 8073  grpinvop 8080  grpinvdiv 8084  grppncan 8090  grpnpcan 8091  grppnpcan2 8092  ablmuldiv 8107  ablnncan 8112  ablmul 8131  ghsubgi 8138  vcz 8189  vcnegsubdi2 8194  vcoprne 8198  nvnegneg 8271  nvsubadd 8275  nvpncan2 8276  nvnncan 8283  nvdif 8293  nvpi 8294  nvabs 8301  nvge0 8302  nv1 8304  nvnd 8319  imsmetlem 8323  ipid 8363  ipcj 8367  lnocoi 8418  cnph 8478  ipasslem5 8494  ipasslem11 8500  ubthlem10 8538  minveclem28 8572  spwpr4OLD 8663  spwpr4aOLD 8664  sincolem 8665  sinper 8690  cosper 8691  sinmpi 8694  cosmpi 8695  sinppi 8696  sinhalfpip 8699  sinhalfpim 8700  coshalfpim 8702  abssinper 8712  shftefif1olem 8741  effoi 8745  hvpncant 8908  hvaddsub4t 8945  his5t 8953  his2subt 8958  bcsALT 9046  norm1t 9121  hhssmetdval 9149  chocuni 9172  pjthlem7 9225  pjthlem8 9226  pjspansnt 9500  fh1t 9561  fh2t 9562  cm2jt 9563  5oalem2 9600  5oalem3 9601  5oalem5 9603  3oalem2 9608  pjv 9650  mayete3 9673  hoaddid1 9712  hosubid1t 9724  hoadddit 9729  honegsubdi2t 9737  hoaddsubt 9742  unoplint 9844  counopt 9845  hmoplint 9866  hmopcot 9948  nlelsh 9993  riesz3 9995  adjco 10033  branmfnt 10038  kbass2t 10050  kbass6t 10054  hmopidmpj 10080  pjsspos 10100  pjclem4 10127  pj3s 10135  strlem1 10177  stcltrlem1 10203  mdexch 10262  irredlem2 10318  ghomf1olem 10396  cayleylem2 10410  infi1 10447  infi1OLD 10448  moec 10461  limfillem2OLD 10608  2wsms 10630  1cat 10692  isfuna 10754

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain