Theorem eqtr3i 2188

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

Syntax hints:   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  3eqtr3i  2194  3eqtr3ri  2195  unundi  3283  unundir  3284  inindi  3339  inindir  3340  difun1  3382  difabs  3386  notab  3392  dfrab2  3397  dif0  3479  difdifdirss  3493  tpidm13  3676  intmin2  3850  univ  4454  iunxpconst  4664  dmres  4905  opabresid  4937  rnresi  4961  cnvcnv  5056  rnresv  5063  cnvsn0  5072  cnvsn  5086  resdmres  5095  coi2  5120  coires1  5121  dfdm2  5138  isarep2  5275  ssimaex  5547  fnreseql  5595  fmptpr  5677  idref  5725  mpompt  5934  caov31  6031  xpexgALT  6101  cnvoprab  6202  frec0g  6365  unfiin  6891  xpfi  6895  endjusym  7061  halfnqq  7351  caucvgprlemm  7609  caucvgprprlemmu  7636  caucvgsr  7743  mvlladdi  8116  8th4div3  9076  nneoor  9293  nummac  9366  numadd  9368  numaddc  9369  nummul1c  9370  decbin0  9461  infrenegsupex  9532  iseqvalcbv  10392  m1expcl2  10477  facnn  10640  fac0  10641  4bc3eq4  10686  fihasheq0  10707  resqrexlemcalc1  10956  sqrt1  10988  sqrt4  10989  sqrt9  10990  infxrnegsupex  11204  isumss2  11334  geo2sum2  11456  geoihalfsum  11463  sin0  11670  efival  11673  ef01bndlem  11697  cos2bnd  11701  sin4lt0  11707  flodddiv4  11871  2prm  12059  znnen  12331  ennnfonelemhf1o  12346  setsslid  12444  metreslem  13020  retopbas  13163  sinhalfpilem  13352  sincos6thpi  13403  sincos3rdpi  13404  lgsdir2lem3  13571