Theorem 3eqtr4d 1520

Description: A deduction from three chained equalities.

Hypotheses

Ref	Expression
3eqtr4d.1	⊢ (φ → A = B)
3eqtr4d.2	⊢ (φ → C = A)
3eqtr4d.3	⊢ (φ → D = B)

Assertion

Ref	Expression
3eqtr4d	⊢ (φ → C = D)

Proof of Theorem 3eqtr4d

Step	Hyp	Ref	Expression
1		3eqtr4d.2	. 2 ⊢ (φ → C = A)
2		3eqtr4d.1	. . 3 ⊢ (φ → A = B)
3		3eqtr4d.3	. . 3 ⊢ (φ → D = B)
4	2, 3	eqtr4d 1513	. 2 ⊢ (φ → A = D)
5	1, 4	eqtrd 1510	1 ⊢ (φ → C = D)

Syntax hints:   → wi 3   = wceq 958

This theorem is referenced by:  3eqtr4a 1535  fnsnfv 3773  fopabco 3838  fopabcos 3839  frsuct 3959  curry1 4104  oasuc 4169  omsuc 4171  oesuc 4172  oaass 4201  odi 4216  nnmsucr 4246  oaabs 4258  alephcard 4878  addcompi 5034  addasspi 5035  mulcompi 5036  mulasspi 5037  distrpi 5038  adddirt 5331  add23t 5349  mul23t 5431  subdirt 5440  mulneg2t 5464  sub23t 5477  sub4t 5488  divasst 5748  divmul13t 5784  divmul24t 5785  divdiv23t 5794  conjmult 5799  zeot 6201  seq1suclem 6317  seq1res 6328  ser1add2 6339  ser1add 6340  2shft 6353  seq1shftid 6357  iooint 6373  seqzval2t 6554  seqzfveq 6555  expp1t 6575  recexpt 6596  sqnegt 6611  subsq2t 6644  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 7979  grpmuldivass 8084  grppnpcan2 8088  abl23 8100  abldiv23 8106  issubgi 8118  subgabl 8119  ablmul 8127  nvmval 8259  nvmdi 8266  nvaddsub4 8277  nvnncan 8279  nvsub 8291  va1cnlem 8341  ipval2 8353  ipcj 8363  sspmval 8388  sspival 8393  sspimsval 8395  lnosub 8416  ipasslem1 8486  ipasslem11 8496  ipsubdir 8504  sspph 8511  ipblnfi 8512  coshalfpip 8696  efgh 8713  eff1lem 8738  hvadd23t 8898  hvsub4t 8901  hvaddsub12t 8902  hvaddsubasst 8905  hvsubdistr1t 8911  his7t 8951  his2sub2t 8954  hhph 9040  hhssabl 9127  hhssnv 9129  chj4t 9453  hoaddcom 9693  hoaddass 9697  hocadddir 9700  hocsubdir 9701  hoadd23t 9704  ho0co 9709  homco1t 9722  homulasst 9723  hoadddirt 9725  hoaddsubasst 9736  unopnormt 9836  braaddt 9864  bramult 9865  brafnmult 9870  kbmult 9874  lnopsub 9893  homco2t 9896  hoddi 9909  lnopm 9920  lnophs 9921  lnopco 9923  lnopco0 9924  hmopst 9940  hmopmt 9941  lnfnsub 9970  cnlnadjlem2 9996  cnlnadjlem6 10000  adjlnopt 10014  adjmult 10020  adjaddt 10021  nmopco 10023  kbass2t 10045  kbass5t 10048  leopnmidt 10066  pjsdi 10078  pjddi 10079  pjadjco 10084  pjss2co 10087  pjorthco 10092  pjadj2co 10127  pj3cor1 10132  strlem3a 10174  hstrlem3a 10182  golem1 10193  mdexch 10257  icmpmon 10715

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