Theorem eqtr3i 2110

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

Syntax hints:   = wceq 1289

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 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070

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

This theorem is referenced by:  3eqtr3i  2116  3eqtr3ri  2117  unundi  3159  unundir  3160  inindi  3215  inindir  3216  difun1  3257  difabs  3261  notab  3267  dfrab2  3272  dif0  3350  difdifdirss  3363  tpidm13  3537  intmin2  3709  univ  4288  iunxpconst  4486  dmres  4721  opabresid  4752  rnresi  4776  cnvcnv  4870  rnresv  4877  cnvsn0  4886  cnvsn  4900  resdmres  4909  coi2  4934  coires1  4935  dfdm2  4952  isarep2  5087  ssimaex  5349  fnreseql  5393  fmptpr  5473  idref  5518  mpt2mpt  5722  caov31  5816  xpexgALT  5886  cnvoprab  5981  frec0g  6144  unfiin  6616  xpfi  6619  djuin  6735  halfnqq  6948  caucvgprlemm  7206  caucvgprprlemmu  7233  caucvgsr  7326  mvlladdi  7679  8th4div3  8605  nneoor  8818  nummac  8890  numadd  8892  numaddc  8893  nummul1c  8894  decbin0  8985  infrenegsupex  9051  iseqvalcbv  9837  m1expcl2  9942  facnn  10100  fac0  10101  4bc3eq4  10146  fihasheq0  10167  resqrexlemcalc1  10412  sqrt1  10444  sqrt4  10445  sqrt9  10446  isumss2  10749  geo2sum2  10870  geoihalfsum  10877  flodddiv4  11027  2prm  11202  znnen  11304