Theorem 3eqtr4d 1564

Description: A deduction from three chained equalities.

Hypotheses

Ref	Expression
3eqtr4d.1	|- (ph -> A = B)
3eqtr4d.2	|- (ph -> C = A)
3eqtr4d.3	|- (ph -> D = B)

Assertion

Ref	Expression
3eqtr4d	|- (ph -> C = D)

Proof of Theorem 3eqtr4d

Step	Hyp	Ref	Expression
1		3eqtr4d.2	. 2 |- (ph -> C = A)
2		3eqtr4d.1	. . 3 |- (ph -> A = B)
3		3eqtr4d.3	. . 3 |- (ph -> D = B)
4	2, 3	eqtr4d 1557	. 2 |- (ph -> A = D)
5	1, 4	eqtrd 1554	1 |- (ph -> C = D)

Syntax hints:   -> wi 3   = wceq 997

This theorem is referenced by:  3eqtr4a 1579  fnsnfv 3824  fopabco 3889  fopabcos 3890  frsuc 4011  curry1 4156  oasuc 4221  omsuc 4223  oesuc 4224  oaass 4253  odi 4268  nnmsucr 4298  oaabs 4310  alephcard 4932  addcompi 5087  addasspi 5088  mulcompi 5089  mulasspi 5090  distrpi 5091  adddir 5384  add23 5402  mul23 5484  subdir 5493  mulneg2 5517  sub23 5530  sub4 5541  divassOLD 5803  divass 5804  divmul13 5840  divmul24 5841  divdiv23 5850  conjmul 5855  zeo 6284  iooin 6397  seq1suclem 6575  seq1res 6586  ser1add2i 6597  ser1addi 6598  2shfti 6611  seq1shftid 6615  seqzval2 6642  seqzfveq 6643  expp1 6663  recexp 6684  sqneg 6699  subsq2 6732  mulre 6867  imcj 6909  absneg 6922  sqabsadd 6938  sqabssub 6939  absresq 6957  absexp 6958  cjdivi 6978  absmax 6987  bccmpl 7052  sumeq2 7075  fsum1ps 7108  fsumadd 7112  csbfsumlem 7116  fsumcom 7118  fsumrev 7119  fsummulc1 7123  fsumdivc 7125  fsumdivcALT 7126  serzrelem 7151  binomlem5 7160  serzf0i 7259  ser1f0i 7260  geolimilem 7325  fsum0diaglem2 7347  fsum0diag4 7351  erelem3 7411  efcji 7426  efexp 7462  resinval 7524  recosval 7525  sinneg 7533  cosneg 7534  efival 7538  addcos 7550  sin2t 7553  cos2t 7554  bopcnlem2 8067  grpmuldivass 8172  grppnpcan2 8176  abl23 8188  abldiv23 8194  issubgi 8206  subgabl 8207  ablmul 8215  nvmval 8347  nvmdi 8354  nvaddsub4 8365  nvnncan 8367  nvsub 8379  va1cnlem 8429  ipval2 8441  ipcj 8451  sspmval 8476  sspival 8481  sspimsval 8483  lnosub 8504  ipasslem1 8574  ipasslem11 8584  ipsubdir 8592  sspph 8599  ipblnfi 8600  coshalfpip 8784  efgh 8801  eff1lem 8826  hvadd23 8986  hvsub4 8989  hvaddsub12 8990  hvaddsubass 8993  hvsubdistr1 8999  his7 9039  his2sub2 9042  hhph 9128  hhssabli 9215  hhssnv 9217  chj4 9541  hoaddcomi 9781  hoaddassi 9785  hocadddiri 9788  hocsubdiri 9789  hoadd23 9792  ho0coi 9797  homco1 9810  homulass 9811  hoadddir 9813  hoaddsubass 9824  unopnorm 9924  braadd 9952  bramul 9953  brafnmul 9958  kbmul 9962  lnopsubi 9981  homco2 9984  hoddii 9997  lnopmi 10008  lnophsi 10009  lnopcoi 10011  lnopco0i 10012  hmops 10028  hmopm 10029  lnfnsubi 10058  cnlnadjlem2 10084  cnlnadjlem6 10088  adjlnop 10102  adjmul 10108  adjadd 10109  nmopcoi 10111  kbass2 10133  kbass5 10136  leopnmid 10154  pjsdii 10166  pjddii 10167  pjadjcoi 10172  pjss2coi 10175  pjorthcoi 10180  pjadj2coi 10216  pj3cor1i 10221  strlem3a 10263  hstrlem3a 10271  golem1 10282  mdexchi 10346  icmpmon 10826

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-cleq 1515

Copyright terms: Public domain