Theorem 3eqtr3 1506

Description: An inference from three chained equalities.

Hypotheses

Ref	Expression
3eqtr3.1	|- A = B
3eqtr3.2	|- A = C
3eqtr3.3	|- B = D

Assertion

Ref	Expression
3eqtr3	|- C = D

Proof of Theorem 3eqtr3

Step	Hyp	Ref	Expression
1		3eqtr3.2	. 2 |- A = C
2		3eqtr3.1	. . 3 |- A = B
3		3eqtr3.3	. . 3 |- B = D
4	2, 3	eqtr 1498	. 2 |- A = D
5	1, 4	eqtr3 1500	1 |- C = D

Syntax hints:   = wceq 958

This theorem is referenced by:  un12 2191  in12 2227  difundi 2260  difundir 2261  difindi 2262  difindir 2263  difun1 2266  dif23 2267  difab 2272  iunab 2601  xp0 3471  caopr12 4067  caopr13 4069  caopr411 4071  caoprdistrr 4073  rankop 4703  kmlem3 4777  cdaassen 4942  xpcdaen 4943  distrpq 5079  1pr 5129  reclem3pr 5170  pn0sr 5222  negneg 5402  mul12 5435  mul01 5443  negdi 5460  negsubdi 5461  ltneg 5615  ixi 5693  recrec 5770  8th4div3 6033  halfpm6th 6034  seq1seqz 6542  seq01 6553  discrlem1 6657  nnesq 6663  nn0opthlem1 6665  sqr2irrlem1 6725  i4 6735  crmul 6741  imi 6825  abs1m 6904  abslem2i 6908  bcpasc2 6967  geolim1i 7238  isupivth 7290  dfef2 7307  erelem6 7324  efm1legeo 7417  efivalt 7447  sin01bndlem1 7468  ruclem16 7526  ruclem25 7535  ipval2 8353  ipid 8359  ip1ilem 8481  ipdirilem 8484  ipasslem10 8495  siilem1 8507  sinhalfpilem 8674  cospi 8677  sincos4thpi 8705  sincos6thpi 8706  eff1o 8743  pilog 8763  hvmul2neg 8910  hvadd12 8919  hvnegdi 8924  normlem1 8971  normlem9 8979  normpar2 9018  polid2 9019  projlem3 9183  projlem18 9198  chjass 9404  chjo 9406  chj12 9440  qlaxr3 9572  hoadd12 9698  lnophmlem2 9937  lnfn0 9966  nmopcoadj2 10030  subsp 10540

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