Theorem eqtr3i 2162

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

Syntax hints:   = wceq 1331

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  3eqtr3i  2168  3eqtr3ri  2169  unundi  3237  unundir  3238  inindi  3293  inindir  3294  difun1  3336  difabs  3340  notab  3346  dfrab2  3351  dif0  3433  difdifdirss  3447  tpidm13  3623  intmin2  3797  univ  4397  iunxpconst  4599  dmres  4840  opabresid  4872  rnresi  4896  cnvcnv  4991  rnresv  4998  cnvsn0  5007  cnvsn  5021  resdmres  5030  coi2  5055  coires1  5056  dfdm2  5073  isarep2  5210  ssimaex  5482  fnreseql  5530  fmptpr  5612  idref  5658  mpompt  5863  caov31  5960  xpexgALT  6031  cnvoprab  6131  frec0g  6294  unfiin  6814  xpfi  6818  endjusym  6981  halfnqq  7218  caucvgprlemm  7476  caucvgprprlemmu  7503  caucvgsr  7610  mvlladdi  7980  8th4div3  8939  nneoor  9153  nummac  9226  numadd  9228  numaddc  9229  nummul1c  9230  decbin0  9321  infrenegsupex  9389  iseqvalcbv  10230  m1expcl2  10315  facnn  10473  fac0  10474  4bc3eq4  10519  fihasheq0  10540  resqrexlemcalc1  10786  sqrt1  10818  sqrt4  10819  sqrt9  10820  infxrnegsupex  11032  isumss2  11162  geo2sum2  11284  geoihalfsum  11291  sin0  11436  efival  11439  ef01bndlem  11463  cos2bnd  11467  sin4lt0  11473  flodddiv4  11631  2prm  11808  znnen  11911  ennnfonelemhf1o  11926  setsslid  12009  metreslem  12549  retopbas  12692  sinhalfpilem  12872  sincos6thpi  12923  sincos3rdpi  12924