Theorem 3eqtr3d 1491

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 1483	. 2 |- (ph -> A = D)
5	1, 4	eqtr3d 1485	1 |- (ph -> C = D)

Syntax hints:   -> wi 3   = wceq 1099

This theorem is referenced by:  csbvarg 1992  csbnestg 2007  csbima12g 3364  csbfv12g 3681  f1ocnvfv1 3817  f1ocnvfv2 3818  csboprg 3925  mapenlem1 4421  mapenlem2 4422  phplem4 4443  php3 4447  cardiun 4782  add12t 5259  add4t 5261  cnegextlem2 5269  csbnegg 5287  addsubasst 5306  mul12t 5341  mul4t 5343  muladdt 5344  negsubdit 5380  nncant 5392  addsub4t 5396  pnncant 5403  ppncant 5404  div13t 5657  divsubdirt 5682  divcan5t 5688  divadddivt 5691  divdivdivt 5692  divdivmult 5702  halfaddsubt 5939  uzindOLD 6107  seq1m1 6207  shftval3t 6236  seqzm1 6432  sqr11 6584  reret 6685  resubt 6692  imsubt 6695  cjsubt 6702  recjt 6704  facnn2t 6827  faclbnd6 6842  sumeq2 6874  fsum1s 6898  fsump1s 6902  fsum3 6913  fsum4 6914  csbfsum 6916  fsummulc2 6923  serz1p 6941  serzsplit 6945  bcxmas 6965  geolimilem 7121  mulc1cncf 7165  efaddlem5 7235  efne0t 7262  sinsubt 7348  cossubt 7349  tgtop11t 7527  ioo2bl 7799  grpideu 7935  grprcan 7945  grpinvid1 7954  grpasscan1OLD 7956  grplcan 7958  isgrp2i 7959  grpasscan1 7960  grpinvop 7963  grppnpcan2 7975  abl4 7989  ablmul 8016  ghgrpilem4 8021  ghgrpi 8022  vcsubdir 8062  vc0 8075  vcm 8077  nvadd12 8120  nvscom 8128  nvmul0or 8149  nvz0 8172  ipid 8232  sspz 8263  lno0 8286  lnomul 8289  ipasslem3 8358  ipasslem4 8359  ipdi 8369  ipassr 8372  ipsubdi 8375  sin2pim 8524  cos2pim 8525  efper 8582  ghomf1olem 8663  mslb1 8823  trnij 8831  hvmul0ort 9043  hvadd12t 9053  hvadd4t 9054  hvmulcomt 9061  hvsubdistr2t 9066  normnegt 9160  chj12t 9586  h1de2b 9606  h1de2bOLD 9607  spanunsn 9633  5oalem2 9731  3oalem2 9739  mayete3 9804  hoadd4t 9841  homul12t 9862  honegnegt 9863  hosubdit 9865  honegsubdit 9867  hosub4t 9870  adj2t 9988  lnopmult 10021  lnopadd 10025  lnfnadd 10101  lnfnmul 10102  cnlnadjlem6 10134  adjlnopt 10148  bra11 10168  leopmult 10193  hmopidmchlem 10203  pjhmopidm 10234  hstnmoct 10274  strlem1 10301  irredlem3 10441

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-gen 955  ax-17 1190  ax-ext 1436

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

Copyright terms: Public domain