Theorem eqtr3i 2212

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 2193	. 2 |- B = A
3		eqtr3i.2	. 2 |- A = C
4	2, 3	eqtri 2210	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 2171

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

This theorem is referenced by:  3eqtr3i  2218  3eqtr3ri  2219  unundi  3311  unundir  3312  inindi  3367  inindir  3368  difun1  3410  difabs  3414  notab  3420  dfrab2  3425  dif0  3508  difdifdirss  3522  tpidm13  3707  intmin2  3885  univ  4491  iunxpconst  4701  dmres  4943  opabresid  4975  rnresi  5000  cnvcnv  5096  rnresv  5103  cnvsn0  5112  cnvsn  5126  resdmres  5135  coi2  5160  coires1  5161  dfdm2  5178  isarep2  5319  ssimaex  5594  fnreseql  5643  fmptpr  5725  idref  5774  mpompt  5984  caov31  6082  xpexgALT  6153  cnvoprab  6254  frec0g  6417  unfiin  6949  xpfi  6953  endjusym  7120  halfnqq  7434  caucvgprlemm  7692  caucvgprprlemmu  7719  caucvgsr  7826  mvlladdi  8200  8th4div3  9163  nneoor  9380  nummac  9453  numadd  9455  numaddc  9456  nummul1c  9457  decbin0  9548  infrenegsupex  9619  iseqvalcbv  10483  m1expcl2  10568  facnn  10734  fac0  10735  4bc3eq4  10780  fihasheq0  10800  resqrexlemcalc1  11050  sqrt1  11082  sqrt4  11083  sqrt9  11084  infxrnegsupex  11298  isumss2  11428  geo2sum2  11550  geoihalfsum  11557  sin0  11764  efival  11767  ef01bndlem  11791  cos2bnd  11795  sin4lt0  11801  flodddiv4  11966  2prm  12154  znnen  12444  ennnfonelemhf1o  12459  setsslid  12558  ressressg  12580  metreslem  14317  retopbas  14460  sinhalfpilem  14649  sincos6thpi  14700  sincos3rdpi  14701  lgsdir2lem3  14868  lgseisenlem1  14887  lgseisenlem2  14888  2lgsoddprmlem2  14891