Theorem 3eqtr3d 1512

Description: A deduction from three chained equalities.

Hypotheses

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

Assertion

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

Proof of Theorem 3eqtr3d

Step	Hyp	Ref	Expression
1		3eqtr3d.2	. 2 |- (ph -> A = C)
2		3eqtr3d.1	. . 3 |- (ph -> A = B)
3		3eqtr3d.3	. . 3 |- (ph -> B = D)
4	2, 3	eqtrd 1504	. 2 |- (ph -> A = D)
5	1, 4	eqtr3d 1506	1 |- (ph -> C = D)

Syntax hints:   -> wi 3   = wceq 954

This theorem is referenced by:  csbvarg 2017  csbnestg 2032  csbima12g 3405  csbfv12g 3733  f1ocnvfv1 3869  f1ocnvfv2 3870  csboprg 3977  mapenlem1 4475  mapenlem2 4476  phplem4 4497  php3 4501  cardiun 4839  add12t 5316  add4t 5318  cnegextlem2 5326  csbnegg 5344  addsubasst 5363  mul12t 5398  mul4t 5400  muladdt 5401  negsubdit 5437  nncant 5449  addsub4t 5453  pnncant 5460  ppncant 5461  div13t 5714  divsubdirt 5739  divcan5t 5745  divadddivt 5748  divdivdivt 5749  divdivmult 5759  halfaddsubt 5996  uzindOLD 6164  seq1m1 6264  shftval3t 6293  seqzm1 6489  sqr11 6641  reret 6742  resubt 6749  imsubt 6752  cjsubt 6759  recjt 6761  facnn2t 6884  faclbnd6 6899  sumeq2 6931  fsum1s 6955  fsump1s 6959  fsum3 6970  fsum4 6971  csbfsum 6973  fsummulc2 6980  serz1p 6998  serzsplit 7002  bcxmas 7022  geolimilem 7178  mulc1cncf 7222  efaddlem5 7292  efne0t 7319  sinsubt 7405  cossubt 7406  tgtop11t 7584  ioo2bl 7864  grpideu 8003  grprcan 8013  grpinvid1 8022  grplcan 8025  isgrp2i 8026  grpasscan1 8027  grpinvop 8030  grppnpcan2 8042  abl4 8056  ablmul 8083  ghgrpilem4 8088  ghgrpi 8089  vcsubdir 8127  vc0 8140  vcm 8142  vcoprne 8150  nvadd12 8194  nvscom 8202  nvmul0or 8224  nvz0 8248  ipid 8310  sspz 8341  lno0 8364  lnomul 8367  ipasslem3 8436  ipasslem4 8437  ipdi 8447  ipassr 8450  ipsubdi 8453  sin2pim 8630  cos2pim 8631  efper 8686  hvmul0ort 8833  hvadd12t 8843  hvadd4t 8844  hvmulcomt 8851  hvsubdistr2t 8856  normnegt 8950  chj12t 9395  h1de2b 9415  h1de2bOLD 9416  spanunsn 9442  5oalem2 9540  3oalem2 9548  mayete3 9613  hoadd4t 9650  homul12t 9671  honegnegt 9672  hosubdit 9674  honegsubdit 9676  hosub4t 9679  adj2t 9797  lnopmult 9830  lnopadd 9834  lnfnadd 9910  lnfnmul 9911  cnlnadjlem6 9943  adjlnopt 9957  adjeq0 9962  bra11 9979  leopmult 10005  hmopidmchlem 10016  pjhmopidm 10048  hstnmoct 10088  strlem1 10115  irredlem3 10256  ghomf1olem 10330  mslb1 10509  trnij 10517

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

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

Copyright terms: Public domain