Theorem 3eqtr4d 1517

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

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  3eqtr4a 1532  fnsnfv 3767  fopabco 3832  fopabcos 3833  frsuct 3953  curry1 4098  oasuc 4163  omsuc 4165  oesuc 4166  oaass 4195  odi 4210  nnmsucr 4240  oaabs 4252  alephcard 4867  addcompi 5022  addasspi 5023  mulcompi 5024  mulasspi 5025  distrpi 5026  adddirt 5319  add23t 5337  mul23t 5419  subdirt 5428  mulneg2t 5452  sub23t 5465  sub4t 5476  divasst 5741  divmul13t 5782  divmul24t 5783  divdiv23t 5792  conjmult 5797  zeot 6199  seq1suclem 6316  seq1res 6327  ser1add2 6338  ser1add 6339  2shft 6352  seq1shftid 6356  iooint 6372  seqzval2t 6553  seqzfveq 6554  expp1t 6574  recexpt 6595  sqnegt 6610  subsq2t 6643  imcjt 6819  absnegt 6832  sqabsaddt 6848  sqabssubt 6849  absresqt 6867  absexpt 6868  cjdiv 6888  absmaxt 6897  bccmplt 6962  sumeq2 6985  fsum1ps 7018  fsumadd 7022  csbfsumlem 7026  fsumcom 7028  fsumrev 7029  fsummulc1 7033  fsumdivc 7035  fsumdivcALT 7036  serzrelem 7061  binomlem5 7070  serzf0 7169  ser1f0 7170  geolimilem 7235  fsum0diaglem2 7257  fsum0diag4 7261  erelem3 7321  efcj 7336  efexpt 7372  resinvalt 7433  recosvalt 7434  sinnegt 7442  cosnegt 7443  efivalt 7447  addcost 7459  sin2tt 7462  cos2tt 7463  bopcnlem2 7982  grpmuldivass 8088  grppnpcan2 8092  abl23 8104  abldiv23 8110  issubgi 8122  subgabl 8123  ablmul 8131  nvmval 8263  nvmdi 8270  nvaddsub4 8281  nvnncan 8283  nvsub 8295  va1cnlem 8345  ipval2 8357  ipcj 8367  sspmval 8392  sspival 8397  sspimsval 8399  lnosub 8420  ipasslem1 8490  ipasslem11 8500  ipsubdir 8508  sspph 8515  ipblnfi 8516  coshalfpip 8701  efgh 8718  eff1lem 8743  hvadd23t 8903  hvsub4t 8906  hvaddsub12t 8907  hvaddsubasst 8910  hvsubdistr1t 8916  his7t 8956  his2sub2t 8959  hhph 9045  hhssabl 9132  hhssnv 9134  chj4t 9458  hoaddcom 9698  hoaddass 9702  hocadddir 9705  hocsubdir 9706  hoadd23t 9709  ho0co 9714  homco1t 9727  homulasst 9728  hoadddirt 9730  hoaddsubasst 9741  unopnormt 9841  braaddt 9869  bramult 9870  brafnmult 9875  kbmult 9879  lnopsub 9898  homco2t 9901  hoddi 9914  lnopm 9925  lnophs 9926  lnopco 9928  lnopco0 9929  hmopst 9945  hmopmt 9946  lnfnsub 9975  cnlnadjlem2 10001  cnlnadjlem6 10005  adjlnopt 10019  adjmult 10025  adjaddt 10026  nmopco 10028  kbass2t 10050  kbass5t 10053  leopnmidt 10071  pjsdi 10083  pjddi 10084  pjadjco 10089  pjss2co 10092  pjorthco 10097  pjadj2co 10132  pj3cor1 10137  strlem3a 10179  hstrlem3a 10187  golem1 10198  mdexch 10262  icmpmon 10744

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