Theorem eqtr3i 2375

Description: An equality transitivity inference. (Contributed by NM, 6-May-1994.)

Hypotheses

Ref	Expression
eqtr3i.1	|- A = B
eqtr3i.2	|- A = C

Assertion

Ref	Expression
eqtr3i	|- B = C

Proof of Theorem eqtr3i

Step	Hyp	Ref	Expression
1		eqtr3i.1	. . 3 |- A = B
2	1	eqcomi 2357	. 2 |- B = A
3		eqtr3i.2	. 2 |- A = C
4	2, 3	eqtri 2373	1 |- B = C

Syntax hints:   = wceq 1642

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  3eqtr3i  2381  3eqtr3ri  2382  unundi  3424  unundir  3425  inindi  3472  inindir  3473  dfin4  3495  difun1  3514  difabs  3518  notab  3525  dfrab2  3530  dif0  3620  difdifdir  3637  tpidm13  3822  intmin2  3953  compl0  4071  1cnnc  4408  tfinltfinlem1  4500  evenodddisj  4516  sfinltfin  4535  iunxpconst  4819  opabbi2i  4866  dmres  4986  opabresid  5003  rnresi  5011  resdmres  5078  coires1  5096  cnvtr  5098  fcoi1  5240  fopabsn  5441  fvsnun1  5447  funiunfv  5467  caov31  5637  oprabbi2i  5647  mpt2mpt  5709  composefn  5818  braddcfn  5826  frds  5935  enpw1  6062  nncdiv3  6277  nnc3n3p1  6278