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-mp 5  ax-1 6  ax-2 7  ax-3 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  3425  unundir  3426  inindi  3473  inindir  3474  dfin4  3496  difun1  3515  difabs  3519  notab  3526  dfrab2  3531  dif0  3621  difdifdir  3638  tpidm13  3823  intmin2  3954  compl0  4072  1cnnc  4409  tfinltfinlem1  4501  evenodddisj  4517  sfinltfin  4536  iunxpconst  4820  opabbi2i  4867  dmres  4987  opabresid  5004  rnresi  5012  resdmres  5079  coires1  5097  cnvtr  5099  fcoi1  5241  fopabsn  5442  fvsnun1  5448  funiunfv  5468  caov31  5638  oprabbi2i  5648  mpt2mpt  5710  composefn  5819  braddcfn  5827  frds  5936  enpw1  6063  nncdiv3  6278  nnc3n3p1  6279