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  7437  halfnqq  7778  caucvgprlemm  8036  caucvgprprlemmu  8063  caucvgsr  8170  mvlladdi  8546  8th4div3  9529  nneoor  9753  nummac  9831  numadd  9833  numaddc  9834  nummul1c  9835  decbin0  9926  infrenegsupex  10004  fz00m1  10462  xnn0nnen  10889  iseqvalcbv  10911  m1expcl2  11013  facnn  11181  fac0  11182  4bc3eq4  11228  fihasheq0  11248  resqrexlemcalc1  11796  sqrt1  11828  sqrt4  11829  sqrt9  11830  infxrnegsupex  12048  isumss2  12179  geo2sum2  12301  geoihalfsum  12308  sin0  12515  efival  12518  ef01bndlem  12542  cos2bnd  12546  sin4lt0  12553  flodddiv4  12722  2prm  12924  dec5dvds  13214  modxai  13218  mod2xi  13219  mod2xnegi  13221  gcdi  13223  numexp2x  13228  decsplit  13232  ballotfilem2  13280  znnen  13341  ennnfonelemhf1o  13356  setsslid  13455  ressressg  13482  metreslem  15572  retopbas  15715  cnfldms  15728  sinhalfpilem  15984  sincos6thpi  16035  sincos3rdpi  16036  log2tlbndlog2  16181  log2ublem2  16183  log2ublog2  16185  cht2  16237  ppiqub  16254  bposlem6  16277  bposlem8  16279  bposlem9  16280  lgsdir2lem3  16315  lgseisenlem1  16355  lgseisenlem2  16356  lgsquadlem1  16362  lgsquadlem2  16363  2lgsoddprmlem2  16391