Theorem eqtr3i 2135

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

Syntax hints:   = wceq 1312

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-4 1468  ax-17 1487  ax-ext 2095

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

This theorem is referenced by:  3eqtr3i  2141  3eqtr3ri  2142  unundi  3201  unundir  3202  inindi  3257  inindir  3258  difun1  3300  difabs  3304  notab  3310  dfrab2  3315  dif0  3397  difdifdirss  3411  tpidm13  3587  intmin2  3761  univ  4355  iunxpconst  4557  dmres  4796  opabresid  4828  rnresi  4852  cnvcnv  4947  rnresv  4954  cnvsn0  4963  cnvsn  4977  resdmres  4986  coi2  5011  coires1  5012  dfdm2  5029  isarep2  5166  ssimaex  5434  fnreseql  5482  fmptpr  5564  idref  5610  mpompt  5815  caov31  5912  xpexgALT  5983  cnvoprab  6083  frec0g  6246  unfiin  6765  xpfi  6769  endjusym  6931  halfnqq  7160  caucvgprlemm  7418  caucvgprprlemmu  7445  caucvgsr  7538  mvlladdi  7897  8th4div3  8837  nneoor  9051  nummac  9124  numadd  9126  numaddc  9127  nummul1c  9128  decbin0  9219  infrenegsupex  9285  iseqvalcbv  10117  m1expcl2  10202  facnn  10360  fac0  10361  4bc3eq4  10406  fihasheq0  10427  resqrexlemcalc1  10672  sqrt1  10704  sqrt4  10705  sqrt9  10706  infxrnegsupex  10918  isumss2  11048  geo2sum2  11170  geoihalfsum  11177  sin0  11281  efival  11284  ef01bndlem  11308  cos2bnd  11312  sin4lt0  11318  flodddiv4  11473  2prm  11648  znnen  11750  ennnfonelemhf1o  11765  setsslid  11846  metreslem  12363  retopbas  12506