Theorem 3eqtr4d 1509

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

Syntax hints:   -> wi 3   = wceq 953

This theorem is referenced by:  3eqtr4a 1524  fnsnfv 3752  fopabco 3817  fopabcos 3818  frsuct 3938  curry1 4082  oasuc 4147  omsuc 4149  oesuc 4150  oaass 4179  odi 4194  nnmsucr 4224  oaabs 4236  alephcard 4839  addcompi 4994  addasspi 4995  mulcompi 4996  mulasspi 4997  distrpi 4998  adddirt 5291  add23t 5309  mul23t 5391  subdirt 5400  mulneg2t 5424  sub23t 5437  sub4t 5448  divasst 5704  divmul13t 5738  divmul24t 5739  divdiv23t 5748  conjmult 5753  zeot 6146  seq1suclem 6253  seq1res 6264  ser1add2 6275  ser1add 6276  2shft 6289  seq1shftid 6293  iooint 6309  seqzval2t 6485  seqzfveq 6486  expp1t 6506  recexpt 6526  sqnegt 6541  subsq2t 6574  imcjt 6754  absnegt 6767  sqabsaddt 6783  sqabssubt 6784  absresqt 6802  absexpt 6803  cjdiv 6826  bccmplt 6900  sumeq2 6923  fsum1ps 6956  fsumadd 6960  csbfsumlem 6964  fsumcom 6966  fsumrev 6967  fsummulc1 6971  fsumdivc 6973  fsumdivcALT 6974  serzrelem 6999  binomlem5 7008  serzf0 7105  ser1f0 7106  geolimilem 7170  fsum0diaglem2 7192  fsum0diag4 7196  erelem3 7263  efcj 7278  efexpt 7314  resinvalt 7375  recosvalt 7376  sinnegt 7384  cosnegt 7385  efivalt 7389  addcost 7401  sin2tt 7404  cos2tt 7405  bopcnlem2 7916  grpmuldivass 8023  grppnpcan2 8027  abl23 8040  abldiv23 8047  issubgi 8059  subgabl 8060  ablmul 8068  nvmval 8203  nvmdi 8210  nvaddsub4 8221  nvnncan 8223  nvsub 8234  va1cnlem 8279  ipval2 8291  ipcj 8301  sspmval 8326  sspival 8331  sspimsval 8333  lnosub 8353  ipasslem1 8421  ipasslem11 8431  ipsubdir 8439  sspph 8446  ipblnfi 8447  coshalfpip 8618  efgh 8633  circgrpOLD 8658  eff1lem 8664  hvadd23t 8824  hvsub4t 8827  hvaddsub12t 8828  hvaddsubasst 8831  hvsubdistr1t 8837  his7t 8877  his2sub2t 8880  hhph 8966  hhssabl 9053  hhssnv 9054  chj4t 9373  hoaddcom 9615  hoaddass 9619  hocadddir 9622  hocsubdir 9623  hoadd23t 9626  ho0co 9631  homco1t 9644  homulasst 9645  hoadddirt 9647  hoaddsubasst 9658  unopnormt 9757  braaddt 9785  bramult 9786  brafnmult 9791  kbmult 9795  lnopsub 9814  homco2t 9817  hoddi 9829  lnopm 9840  lnophs 9841  lnopco 9843  lnopco0 9844  hmopst 9860  hmopmt 9861  lnfnsub 9890  cnlnadjlem2 9916  cnlnadjlem6 9920  adjlnopt 9934  adjmult 9939  adjaddt 9940  nmopco 9942  kbass2t 9962  kbass5t 9965  leopnmidt 9982  pjsdi 9994  pjddi 9995  pjadjco 10000  pjss2co 10003  pjorthco 10008  pjadj2co 10042  pj3cor1 10047  strlem3a 10089  hstrlem3a 10097  golem1 10108  mdexch 10170  icmpmon 10587

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

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

Copyright terms: Public domain