Theorem eqtr3i 2216

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

Syntax hints:   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  3eqtr3i  2222  3eqtr3ri  2223  unundi  3320  unundir  3321  inindi  3376  inindir  3377  difun1  3419  difabs  3423  notab  3429  dfrab2  3434  dif0  3517  difdifdirss  3531  tpidm13  3718  intmin2  3896  univ  4507  iunxpconst  4719  dmres  4963  rnresi  5022  cnvcnv  5118  rnresv  5125  cnvsn0  5134  cnvsn  5148  resdmres  5157  coi2  5182  coires1  5183  dfdm2  5200  isarep2  5341  ssimaex  5618  fnreseql  5668  fmptpr  5750  idref  5799  mpompt  6010  caov31  6108  xpexgALT  6185  cnvoprab  6287  frec0g  6450  unfiin  6982  xpfi  6986  endjusym  7155  halfnqq  7470  caucvgprlemm  7728  caucvgprprlemmu  7755  caucvgsr  7862  mvlladdi  8237  8th4div3  9201  nneoor  9419  nummac  9492  numadd  9494  numaddc  9495  nummul1c  9496  decbin0  9587  infrenegsupex  9659  xnn0nnen  10508  iseqvalcbv  10530  m1expcl2  10632  facnn  10798  fac0  10799  4bc3eq4  10844  fihasheq0  10864  resqrexlemcalc1  11158  sqrt1  11190  sqrt4  11191  sqrt9  11192  infxrnegsupex  11406  isumss2  11536  geo2sum2  11658  geoihalfsum  11665  sin0  11872  efival  11875  ef01bndlem  11899  cos2bnd  11903  sin4lt0  11910  flodddiv4  12075  2prm  12265  znnen  12555  ennnfonelemhf1o  12570  setsslid  12669  ressressg  12693  mpocnfldadd  14053  mpocnfldmul  14055  metreslem  14548  retopbas  14691  sinhalfpilem  14926  sincos6thpi  14977  sincos3rdpi  14978  lgsdir2lem3  15146  lgseisenlem1  15186  lgseisenlem2  15187  lgsquadlem1  15191  2lgsoddprmlem2  15194