Theorem eqtr3i 2104

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 2086	. 2 |- B = A
3		eqtr3i.2	. 2 |- A = C
4	2, 3	eqtri 2102	1 |- B = C

Syntax hints:   = wceq 1285

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-cleq 2075

This theorem is referenced by:  3eqtr3i  2110  3eqtr3ri  2111  unundi  3134  unundir  3135  inindi  3190  inindir  3191  difun1  3231  difabs  3235  notab  3241  dfrab2  3246  dif0  3321  difdifdirss  3334  tpidm13  3500  intmin2  3670  univ  4233  iunxpconst  4426  dmres  4660  opabresid  4689  rnresi  4712  cnvcnv  4803  rnresv  4810  cnvsn0  4819  cnvsn  4833  resdmres  4842  coi2  4867  coires1  4868  dfdm2  4882  isarep2  5017  ssimaex  5266  fnreseql  5309  fmptpr  5387  idref  5428  mpt2mpt  5627  caov31  5721  xpexgALT  5791  cnvoprab  5886  frec0g  6046  unfiin  6444  halfnqq  6662  caucvgprlemm  6920  caucvgprprlemmu  6947  caucvgsr  7040  mvlladdi  7393  8th4div3  8317  nneoor  8530  nummac  8602  numadd  8604  numaddc  8605  nummul1c  8606  decbin0  8697  infrenegsupex  8763  iseqvalcbv  9531  m1expcl2  9595  facnn  9751  fac0  9752  4bc3eq4  9797  sizeeq0  9818  resqrexlemcalc1  10038  sqrt1  10070  sqrt4  10071  sqrt9  10072  flodddiv4  10478  2prm  10653  znnen  10709