Theorem 3eqtr4 1126

Description: An inference from three chained equalities.

Hypotheses

Ref	Expression
3eqtr4.1	⊢ A = B
3eqtr4.2	⊢ C = A
3eqtr4.3	⊢ D = B

Assertion

Ref	Expression
3eqtr4	⊢ C = D

Proof of Theorem 3eqtr4

Step	Hyp	Ref	Expression
1		3eqtr4.2	. 2 ⊢ C = A
2		3eqtr4.1	. . 3 ⊢ A = B
3		3eqtr4.3	. . 3 ⊢ D = B
4	2, 3	eqtr4 1122	. 2 ⊢ A = D
5	1, 4	eqtr 1119	1 ⊢ C = D

Syntax hints:   = wceq 1091

This theorem is referenced by:  birabi 1342  cbvrab 1425  un23 1617  un4 1618  in23 1652  in4 1653  indir 1678  undir 1679  unrab 1694  difrab 1695  dfnul3 1710  difdifdir 1765  prcom 1840  pwpw0 1883  int0 1978  dfiun2 2014  dfiin2 2015  cbviunv 2016  cbvopab 2104  cbvopab1 2106  cbvopab1s 2107  cbvopab1v 2108  cbvopab2v 2109  unopab 2121  dfom2 2374  xpundi 2461  xpundir 2462  cnvco 2520  dm0 2542  dmsn0 2543  dmsnsn0 2544  dmi 2545  resundi 2582  resundir 2583  rescom 2588  resima 2595  imadmrn 2610  rnun 2644  imaun 2647  co01 2664  zfrep6 2744  tz7.44-2 2967  tz7.44-3 2968  rdglem2 2976  frfnom 2989  dfoprab2 3021  cbvoprab12 3028  cbvoprab3v 3030  caopr32 3074  caopr31 3076  caopr4 3078  caoprlem2 3083  fo1st 3094  fo2nd 3095  ec2 3203  qsex 3231  snec 3232  map0e 3266  sbthlem6 3354  unfilem1 3438  ranksn 3532  numthlem 3598  alephcard 3673  xp2cda 3723  dmaddpi 3812  dmmulpi 3813  addasspq 3857  genpdm 3899  prlem936 3949  m1p1sr 3995  m1m1sr 3996  mulgt0sr 4008  axrecex 4079  axi2m1 4082  subdir 4183  mulneg1 4190  negdi3 4195  sub4 4206  divdistr 4243  divdiv23 4272  3p3e6 4493  4p3e7 4495  4p4e8 4496  5p3e8 4498  5p4e9 4499  6p3e9 4501  crmult 4530  sqmul 4688  sqdiv 4689  sqreci 4690  binom 4712  sqr0 4730  sqrlem16 4746  cjcj 4808  recj 4812  imcj 4813  readd 4814  imadd 4815  cjadd 4818  cjmul 4819  cjmulrcl 4821  reneg 4824  imneg 4826  cjneg 4827  addcj 4828  absneg 4843  abscj 4844  absmul 4846  sqabsadd 4847  abs3dif 4860  hvsubdistr1 5024  hvsubass 5027  hvsub23 5028  hvsubsub4 5031  hv2times 5033  hvnegdi 5034  normlem3 5065  normlem9 5070  norm-iii 5087  norm3dif 5094  normpar 5099  normpar2 5100  occllem1 5180  projlem3 5195  pjthlem5 5229  pjthlem14 5238  chjass 5407  h1de2 5458  spanunsn 5482  fh1 5518  qlax4 5523  qlaxr3 5529  3oalem5 5556  pjadj 5564  pjsub 5569  pjcj 5575  pjrn 5587  hosdass 5621

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org