Theorem eqtr3i 2227

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 2208	. 2 ⊢ 𝐵 = 𝐴
3		eqtr3i.2	. 2 ⊢ 𝐴 = 𝐶
4	2, 3	eqtri 2225	1 ⊢ 𝐵 = 𝐶

Syntax hints:   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  3eqtr3i  2233  3eqtr3ri  2234  unundi  3333  unundir  3334  inindi  3389  inindir  3390  difun1  3432  difabs  3436  notab  3442  dfrab2  3447  dif0  3530  difdifdirss  3544  tpidm13  3732  intmin2  3910  univ  4522  iunxpconst  4734  dmres  4979  rnresi  5038  cnvcnv  5134  rnresv  5141  cnvsn0  5150  cnvsn  5164  resdmres  5173  coi2  5198  coires1  5199  dfdm2  5216  isarep2  5360  ssimaex  5639  fnreseql  5689  fmptpr  5775  idref  5824  mpompt  6036  caov31  6135  xpexgALT  6217  cnvoprab  6319  frec0g  6482  unfiin  7022  xpfi  7028  endjusym  7197  halfnqq  7522  caucvgprlemm  7780  caucvgprprlemmu  7807  caucvgsr  7914  mvlladdi  8289  8th4div3  9255  nneoor  9474  nummac  9547  numadd  9549  numaddc  9550  nummul1c  9551  decbin0  9642  infrenegsupex  9714  xnn0nnen  10580  iseqvalcbv  10602  m1expcl2  10704  facnn  10870  fac0  10871  4bc3eq4  10916  fihasheq0  10936  resqrexlemcalc1  11296  sqrt1  11328  sqrt4  11329  sqrt9  11330  infxrnegsupex  11545  isumss2  11675  geo2sum2  11797  geoihalfsum  11804  sin0  12011  efival  12014  ef01bndlem  12038  cos2bnd  12042  sin4lt0  12049  flodddiv4  12218  2prm  12420  dec5dvds  12706  modxai  12710  mod2xi  12711  gcdi  12714  numexp2x  12719  decsplit  12723  znnen  12740  ennnfonelemhf1o  12755  setsslid  12854  ressressg  12878  metreslem  14823  retopbas  14966  cnfldms  14979  sinhalfpilem  15234  sincos6thpi  15285  sincos3rdpi  15286  lgsdir2lem3  15478  lgseisenlem1  15518  lgseisenlem2  15519  lgsquadlem1  15525  lgsquadlem2  15526  2lgsoddprmlem2  15554