Theorem eqtr3i 2198

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 2179	. 2 |- B = A
3		eqtr3i.2	. 2 |- A = C
4	2, 3	eqtri 2196	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 1445  ax-gen 1447  ax-4 1508  ax-17 1524  ax-ext 2157

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

This theorem is referenced by:  3eqtr3i  2204  3eqtr3ri  2205  unundi  3294  unundir  3295  inindi  3350  inindir  3351  difun1  3393  difabs  3397  notab  3403  dfrab2  3408  dif0  3491  difdifdirss  3505  tpidm13  3689  intmin2  3866  univ  4470  iunxpconst  4680  dmres  4921  opabresid  4953  rnresi  4978  cnvcnv  5073  rnresv  5080  cnvsn0  5089  cnvsn  5103  resdmres  5112  coi2  5137  coires1  5138  dfdm2  5155  isarep2  5295  ssimaex  5569  fnreseql  5618  fmptpr  5700  idref  5748  mpompt  5957  caov31  6054  xpexgALT  6124  cnvoprab  6225  frec0g  6388  unfiin  6915  xpfi  6919  endjusym  7085  halfnqq  7384  caucvgprlemm  7642  caucvgprprlemmu  7669  caucvgsr  7776  mvlladdi  8149  8th4div3  9109  nneoor  9326  nummac  9399  numadd  9401  numaddc  9402  nummul1c  9403  decbin0  9494  infrenegsupex  9565  iseqvalcbv  10425  m1expcl2  10510  facnn  10673  fac0  10674  4bc3eq4  10719  fihasheq0  10739  resqrexlemcalc1  10989  sqrt1  11021  sqrt4  11022  sqrt9  11023  infxrnegsupex  11237  isumss2  11367  geo2sum2  11489  geoihalfsum  11496  sin0  11703  efival  11706  ef01bndlem  11730  cos2bnd  11734  sin4lt0  11740  flodddiv4  11904  2prm  12092  znnen  12364  ennnfonelemhf1o  12379  setsslid  12477  metreslem  13431  retopbas  13574  sinhalfpilem  13763  sincos6thpi  13814  sincos3rdpi  13815  lgsdir2lem3  13982