Theorem eqtr3i 2062

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

Syntax hints:   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  3eqtr3i  2068  3eqtr3ri  2069  unundi  3104  unundir  3105  inindi  3154  inindir  3155  difun1  3197  difabs  3201  notab  3207  dfrab2  3212  dif0  3294  difdifdirss  3307  tpidm13  3470  intmin2  3641  univ  4207  iunxpconst  4400  dmres  4632  opabresid  4659  rnresi  4682  cnvcnv  4773  rnresv  4780  cnvsn0  4789  cnvsn  4803  resdmres  4812  coi2  4837  coires1  4838  dfdm2  4852  isarep2  4986  ssimaex  5234  fnreseql  5277  fmptpr  5355  idref  5396  mpt2mpt  5596  caov31  5690  xpexgALT  5760  frec0g  5983  halfnqq  6508  caucvgprlemm  6766  caucvgprprlemmu  6793  caucvgsr  6886  mvlladdi  7229  8th4div3  8144  nneoor  8340  dec10  8397  nummac  8399  numadd  8401  numaddc  8402  nummul1c  8403  9p2e11  8429  decbin0  8470  m1expcl2  9277  resqrexlemcalc1  9612  sqrt1  9644  sqrt4  9645  sqrt9  9646