Theorem eqtr3i 2103

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

Syntax hints:   = wceq 1284

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 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

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

This theorem is referenced by:  3eqtr3i  2109  3eqtr3ri  2110  unundi  3133  unundir  3134  inindi  3183  inindir  3184  difun1  3224  difabs  3228  notab  3234  dfrab2  3239  dif0  3314  difdifdirss  3327  tpidm13  3492  intmin2  3662  univ  4225  iunxpconst  4418  dmres  4650  opabresid  4679  rnresi  4702  cnvcnv  4793  rnresv  4800  cnvsn0  4809  cnvsn  4823  resdmres  4832  coi2  4857  coires1  4858  dfdm2  4872  isarep2  5006  ssimaex  5255  fnreseql  5298  fmptpr  5376  idref  5417  mpt2mpt  5616  caov31  5710  xpexgALT  5780  cnvoprab  5875  frec0g  6006  halfnqq  6600  caucvgprlemm  6858  caucvgprprlemmu  6885  caucvgsr  6978  mvlladdi  7326  8th4div3  8250  nneoor  8449  nummac  8521  numadd  8523  numaddc  8524  nummul1c  8525  decbin0  8616  infrenegsupex  8682  m1expcl2  9498  facnn  9654  fac0  9655  4bc3eq4  9700  resqrexlemcalc1  9900  sqrt1  9932  sqrt4  9933  sqrt9  9934  flodddiv4  10334  2prm  10509