Theorem eqtr3i 2163

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

Syntax hints:   = wceq 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133

This theorem is referenced by:  3eqtr3i  2169  3eqtr3ri  2170  unundi  3242  unundir  3243  inindi  3298  inindir  3299  difun1  3341  difabs  3345  notab  3351  dfrab2  3356  dif0  3438  difdifdirss  3452  tpidm13  3631  intmin2  3805  univ  4405  iunxpconst  4607  dmres  4848  opabresid  4880  rnresi  4904  cnvcnv  4999  rnresv  5006  cnvsn0  5015  cnvsn  5029  resdmres  5038  coi2  5063  coires1  5064  dfdm2  5081  isarep2  5218  ssimaex  5490  fnreseql  5538  fmptpr  5620  idref  5666  mpompt  5871  caov31  5968  xpexgALT  6039  cnvoprab  6139  frec0g  6302  unfiin  6822  xpfi  6826  endjusym  6989  halfnqq  7242  caucvgprlemm  7500  caucvgprprlemmu  7527  caucvgsr  7634  mvlladdi  8004  8th4div3  8963  nneoor  9177  nummac  9250  numadd  9252  numaddc  9253  nummul1c  9254  decbin0  9345  infrenegsupex  9416  iseqvalcbv  10261  m1expcl2  10346  facnn  10505  fac0  10506  4bc3eq4  10551  fihasheq0  10572  resqrexlemcalc1  10818  sqrt1  10850  sqrt4  10851  sqrt9  10852  infxrnegsupex  11064  isumss2  11194  geo2sum2  11316  geoihalfsum  11323  sin0  11472  efival  11475  ef01bndlem  11499  cos2bnd  11503  sin4lt0  11509  flodddiv4  11667  2prm  11844  znnen  11947  ennnfonelemhf1o  11962  setsslid  12048  metreslem  12588  retopbas  12731  sinhalfpilem  12920  sincos6thpi  12971  sincos3rdpi  12972