Theorem 3eqtrd 1514

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

Syntax hints:   -> wi 3   = wceq 958

This theorem is referenced by:  csbnestg 2039  csbopabg 2683  csbima12g 3419  resiima 3425  csbfv12g 3748  csboprg 3992  om1 4182  oe1 4184  oarec 4202  nneob 4261  ltexpq 5092  halfpq 5094  addsubt 5396  muladdt 5433  negsubdi2t 5470  nnncan1t 5479  mulsubt 5489  recextlem1 5694  muleqaddt 5712  div23t 5749  div12t 5751  divdivdivt 5787  conjmult 5799  nndivtrt 5962  uzindOLD 6210  fldivt 6256  uzrdgsuc 6305  seqz1 6548  seqzp1 6549  seq0p1 6552  seqzval2t 6554  mulexpt 6595  divexpt 6600  imret 6774  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 7483  demoivre 7485  cnconst 7777  grpidinvlem1 8045  grpinvid2 8069  grpinvop 8076  grpinvdiv 8080  grppncan 8086  grpnpcan 8087  grppnpcan2 8088  ablmuldiv 8103  ablnncan 8108  ablmul 8127  ghsubgi 8134  vcz 8185  vcnegsubdi2 8190  vcoprne 8194  nvnegneg 8267  nvsubadd 8271  nvpncan2 8272  nvnncan 8279  nvdif 8289  nvpi 8290  nvabs 8297  nvge0 8298  nv1 8300  nvnd 8315  imsmetlem 8319  ipid 8359  ipcj 8363  lnocoi 8414  cnph 8474  ipasslem5 8490  ipasslem11 8496  ubthlem10 8534  minveclem28 8568  spwpr4OLD 8658  spwpr4aOLD 8659  sincolem 8660  sinper 8685  cosper 8686  sinmpi 8689  cosmpi 8690  sinppi 8691  sinhalfpip 8694  sinhalfpim 8695  coshalfpim 8697  abssinper 8707  shftefif1olem 8736  effoi 8740  hvpncant 8903  hvaddsub4t 8940  his5t 8948  his2subt 8953  bcsALT 9041  norm1t 9116  hhssmetdval 9144  chocuni 9167  pjthlem7 9220  pjthlem8 9221  pjspansnt 9495  fh1t 9556  fh2t 9557  cm2jt 9558  5oalem2 9595  5oalem3 9596  5oalem5 9598  3oalem2 9603  pjv 9645  mayete3 9668  hoaddid1 9707  hosubid1t 9719  hoadddit 9724  honegsubdi2t 9732  hoaddsubt 9737  unoplint 9839  counopt 9840  hmoplint 9861  hmopcot 9943  nlelsh 9988  riesz3 9990  adjco 10028  branmfnt 10033  kbass2t 10045  kbass6t 10049  hmopidmpj 10075  pjsspos 10095  pjclem4 10122  pj3s 10130  strlem1 10172  stcltrlem1 10198  mdexch 10257  irredlem2 10313  ghomf1olem 10391  cayleylem2 10405  infi1 10441  moec 10451  limfillem2OLD 10579  2wsms 10601  1cat 10663  isfuna 10725

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

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

Copyright terms: Public domain