Theorem eqtr3i 2200

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

Syntax hints:   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  3eqtr3i  2206  3eqtr3ri  2207  unundi  3296  unundir  3297  inindi  3352  inindir  3353  difun1  3395  difabs  3399  notab  3405  dfrab2  3410  dif0  3493  difdifdirss  3507  tpidm13  3692  intmin2  3870  univ  4476  iunxpconst  4686  dmres  4928  opabresid  4960  rnresi  4985  cnvcnv  5081  rnresv  5088  cnvsn0  5097  cnvsn  5111  resdmres  5120  coi2  5145  coires1  5146  dfdm2  5163  isarep2  5303  ssimaex  5577  fnreseql  5626  fmptpr  5708  idref  5757  mpompt  5966  caov31  6063  xpexgALT  6133  cnvoprab  6234  frec0g  6397  unfiin  6924  xpfi  6928  endjusym  7094  halfnqq  7408  caucvgprlemm  7666  caucvgprprlemmu  7693  caucvgsr  7800  mvlladdi  8174  8th4div3  9137  nneoor  9354  nummac  9427  numadd  9429  numaddc  9430  nummul1c  9431  decbin0  9522  infrenegsupex  9593  iseqvalcbv  10456  m1expcl2  10541  facnn  10706  fac0  10707  4bc3eq4  10752  fihasheq0  10772  resqrexlemcalc1  11022  sqrt1  11054  sqrt4  11055  sqrt9  11056  infxrnegsupex  11270  isumss2  11400  geo2sum2  11522  geoihalfsum  11529  sin0  11736  efival  11739  ef01bndlem  11763  cos2bnd  11767  sin4lt0  11773  flodddiv4  11938  2prm  12126  znnen  12398  ennnfonelemhf1o  12413  setsslid  12512  ressressg  12533  metreslem  13850  retopbas  13993  sinhalfpilem  14182  sincos6thpi  14233  sincos3rdpi  14234  lgsdir2lem3  14401  lgseisenlem1  14420  lgseisenlem2  14421  2lgsoddprmlem2  14424