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 2040  csbopabg 2684  csbima12g 3420  resiima 3426  csbfv12g 3749  csboprg 3993  om1 4183  oe1 4185  oarec 4203  nneob 4262  ltexpq 5099  halfpq 5101  addsubt 5403  muladdt 5440  negsubdi2t 5477  nnncan1t 5486  mulsubt 5496  recextlem1 5701  muleqaddt 5719  div23t 5756  div12t 5758  divdivdivt 5794  conjmult 5806  nndivtrt 5969  uzindOLD 6217  fldivt 6263  uzrdgsuc 6312  seqz1 6555  seqzp1 6556  seq0p1 6559  seqzval2t 6561  mulexpt 6602  divexpt 6607  imret 6781  cjreimt 6835  cjreim2t 6836  cjdiv 6895  ser1absdiflem 6936  facp1t 6943  bcn0t 6970  bcnp11t 6972  fsum1 7012  fsump1 7013  fsumshft 7038  fsumconst 7045  binomlem1 7073  binomlem2 7074  binomlem6 7078  isumnul 7210  fnsmntlem 7232  geoisumr 7250  efcltlem1 7311  ef0lem 7317  efaddlem5 7349  ef01tllem1 7390  abspef01tlub 7402  efi4pt 7442  resin4pt 7443  recos4pt 7444  efmivalt 7455  efeult 7456  absefit 7490  demoivre 7492  cnconst 7784  grpidinvlem1 8052  grpinvid2 8076  grpinvop 8083  grpinvdiv 8087  grppncan 8093  grpnpcan 8094  grppnpcan2 8095  ablmuldiv 8110  ablnncan 8115  ablmul 8134  ghsubgi 8141  vcz 8192  vcnegsubdi2 8197  vcoprne 8201  nvnegneg 8274  nvsubadd 8278  nvpncan2 8279  nvnncan 8286  nvdif 8296  nvpi 8297  nvabs 8304  nvge0 8305  nv1 8307  nvnd 8322  imsmetlem 8326  ipid 8366  ipcj 8370  lnocoi 8421  cnph 8481  ipasslem5 8497  ipasslem11 8503  ubthlem10 8541  minveclem28 8575  spwpr4OLD 8665  spwpr4aOLD 8666  sincolem 8667  sinper 8692  cosper 8693  sinmpi 8696  cosmpi 8697  sinppi 8698  sinhalfpip 8701  sinhalfpim 8702  coshalfpim 8704  abssinper 8714  shftefif1olem 8743  effoi 8747  hvpncant 8910  hvaddsub4t 8947  his5t 8955  his2subt 8960  bcsALT 9048  norm1t 9123  hhssmetdval 9151  chocuni 9174  pjthlem7 9227  pjthlem8 9228  pjspansnt 9502  fh1t 9563  fh2t 9564  cm2jt 9565  5oalem2 9602  5oalem3 9603  5oalem5 9605  3oalem2 9610  pjv 9652  mayete3 9675  hoaddid1 9714  hosubid1t 9726  hoadddit 9731  honegsubdi2t 9739  hoaddsubt 9744  unoplint 9846  counopt 9847  hmoplint 9868  hmopcot 9950  nlelsh 9995  riesz3 9997  adjco 10035  branmfnt 10040  kbass2t 10052  kbass6t 10056  hmopidmpj 10082  pjsspos 10102  pjclem4 10130  pj3s 10138  strlem1 10180  stcltrlem1 10206  mdexch 10265  irredlem2 10321  ghomf1olem 10399  cayleylem2 10413  infi1 10449  moec 10459  limfillem2OLD 10587  2wsms 10609  1cat 10671  isfuna 10733

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