Theorem eqtr3i 2261

Description: An equality transitivity inference. (Contributed by NM, 6-May-1994.)

Hypotheses

Ref	Expression
eqtr3i.1	⊢ 𝐴 = 𝐵
eqtr3i.2	⊢ 𝐴 = 𝐶

Assertion

Ref	Expression
eqtr3i	⊢ 𝐵 = 𝐶

Proof of Theorem eqtr3i

Step	Hyp	Ref	Expression
1		eqtr3i.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	eqcomi 2242	. 2 ⊢ 𝐵 = 𝐴
3		eqtr3i.2	. 2 ⊢ 𝐴 = 𝐶
4	2, 3	eqtri 2259	1 ⊢ 𝐵 = 𝐶

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtr3i  2267  3eqtr3ri  2268  unundi  3390  unundir  3391  inindi  3448  inindir  3449  difun1  3491  difabs  3495  notab  3503  dfrab2  3508  dif0  3596  difdifdirss  3612  tpidm13  3811  intmin2  3996  univ  4622  iunxpconst  4835  dmres  5084  rnresi  5144  cnvcnv  5240  rnresv  5247  cnvsn0  5256  cnvsn  5270  resdmres  5279  coi2  5304  coires1  5305  dfdm2  5322  isarep2  5468  ssimaex  5764  fnreseql  5819  fmptpr  5907  idref  5962  mpompt  6180  caov31  6279  xpexgALT  6366  cnvoprab  6470  frec0g  6668  unfiin  7233  xpfi  7239  endjusym  7436  halfnqq  7777  caucvgprlemm  8035  caucvgprprlemmu  8062  caucvgsr  8169  mvlladdi  8544  8th4div3  9524  nneoor  9748  nummac  9821  numadd  9823  numaddc  9824  nummul1c  9825  decbin0  9916  infrenegsupex  9994  fz00m1  10451  xnn0nnen  10874  iseqvalcbv  10896  m1expcl2  10998  facnn  11165  fac0  11166  4bc3eq4  11212  fihasheq0  11232  resqrexlemcalc1  11780  sqrt1  11812  sqrt4  11813  sqrt9  11814  infxrnegsupex  12029  isumss2  12160  geo2sum2  12282  geoihalfsum  12289  sin0  12496  efival  12499  ef01bndlem  12523  cos2bnd  12527  sin4lt0  12534  flodddiv4  12703  2prm  12905  dec5dvds  13191  modxai  13195  mod2xi  13196  gcdi  13199  numexp2x  13204  decsplit  13208  ballotfilem2  13228  znnen  13289  ennnfonelemhf1o  13304  setsslid  13403  ressressg  13429  metreslem  15481  retopbas  15624  cnfldms  15637  sinhalfpilem  15892  sincos6thpi  15943  sincos3rdpi  15944  log2tlbndlog2  16082  log2ublem2  16084  log2ublog2  16086  lgsdir2lem3  16149  lgseisenlem1  16189  lgseisenlem2  16190  lgsquadlem1  16196  lgsquadlem2  16197  2lgsoddprmlem2  16225