Theorem eqtr2i 2785

Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)

Hypotheses

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

Assertion

Ref	Expression
eqtr2i	⊢ 𝐶 = 𝐴

Proof of Theorem eqtr2i

Step	Hyp	Ref	Expression
1		eqtr2i.1	. . 3 ⊢ 𝐴 = 𝐵
2		eqtr2i.2	. . 3 ⊢ 𝐵 = 𝐶
3	1, 2	eqtri 2784	. 2 ⊢ 𝐴 = 𝐶
4	3	eqcomi 2770	1 ⊢ 𝐶 = 𝐴

Syntax hints:   = wceq 1559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  3eqtrri  2789  3eqtr2ri  2791  dfun3  4226  dfif3  4492  dfsn2  4592  prprc1  4721  diftpsn3  4759  ssunpr  4789  sstp  4791  unidif0OLD  5314  xpindi  5801  xpindir  5802  dmcnvcnv  5905  rncnvcnv  5906  imainrect  6162  dfrn4  6184  predres  6321  fcoi1  6733  foimacnv  6819  f1ossf1o  7105  fsnunfv  7166  difex2  7738  dfoprab3  8030  offval22  8061  suppvalbr  8138  fvmpocurryd  8245  mapsnconst  8868  sbthlem8  9060  fiint  9265  ordtypecbv  9459  trcl  9677  rankxplim2  9832  infdju1  10140  cfval2  10211  itunitc  10372  ituniiun  10373  hsmex2  10384  ltexnq  10927  ixi  11810  zeo  12653  num0h  12694  dec10p  12730  fseq1p1m1  13597  cats1fvn  14865  s3fn  14918  sgnneg  15104  fsumrelem  15826  ef0lem  16099  ef01bndlem  16207  sadcadd  16483  sadadd2  16485  3lcm2e6woprm  16640  mod2xnegi  17098  str0  17216  ressinbas  17272  mreexexlem4d  17670  0g0  18689  frmdplusg  18879  smndex1bas  18934  sgrp2nmndlem4  18956  sgrp2nmndlem5  18957  oppgplusfval  19379  symgsubmefmnd  19429  psgnsn  19551  psgnprfval1  19553  frgpnabllem1  19904  opprmulfval  20375  opprrngb  20382  opprringb  20384  opprunit  20413  00lsp  21036  chrval  21563  dsmmelbas  21779  ltbwe  22085  ply1plusgfvi  22291  mat2pmatfval  22771  unisngl  23575  qtopres  23746  ufildr  23979  oppgtmd  24145  tgioo  24844  tgqioo  24848  dveflem  26029  lhop1lem  26063  sincos4thpi  26566  coskpi  26576  cxpsqrtlem  26755  log2ublem1  26999  efrlim  27022  basellem3  27135  bposlem9  27344  madeun  27965  precsexlem11  28298  graop  29187  0grsubgr  29436  usgrfilem  29485  finsumvtxdg2ssteplem4  29706  wlkvtxedg  29801  2wlkdlem1  30082  2pthd  30097  wlk2v2e  30316  3wlkdlem1  30318  3pthd  30333  konigsberg  30416  cnidOLD  30742  ip1ilem  30986  ipasslem10  30999  normlem6  31275  dfhnorm2  31282  h1de2i  31713  spansnji  31806  pjneli  31883  mayetes3i  31889  pjclem1  32355  mdslmd3i  32492  atabsi  32561  imadifxp  32761  dfdec100  32993  dpmul100  33035  dpmul1000  33037  dpmul4  33052  xrge00  33153  cyc2fv1  33262  cyc2fv2  33263  cyc3fv3  33280  opprlidlabs  33634  vieta  33838  cos9thpiminplylem5  34044  locfinref  34099  cnvordtrestixx  34171  raddcn  34187  rrhcn  34255  qqtopn  34269  esumpfinvallem  34332  sxbrsigalem1  34543  eulerpartgbij  34630  hgt750lem2  34907  subfacp1lem1  35490  subfacval2  35498  quad3  35981  ptrest  38079  poimirlem3  38083  poimirlem8  38088  poimirlem15  38095  mblfinlem3  38119  ismblfin  38121  areacirc  38173  pmapglb  40355  dvh4dimN  42032  hdmapfval  42412  12gcd5e1  42581  sqdeccom12  42859  remul02  42975  mapfzcons1  43259  lmhmlnmsplit  43625  pwssplit4  43627  clcnvlem  44160  cnvrcl0  44162  sqrtcval2  44179  resqrtvalex  44182  imsqrtvalex  44183  iunrelexp0  44239  sumnnodd  46167  climinf2mpt  46249  climinfmpt  46250  dvnmul  46478  wallispilem4  46603  dirkertrigeqlem3  46635  fourierdlem24  46666  fourierdlem57  46698  fourierdlem58  46699  fourierdlem80  46721  fourierswlem  46765  fouriersw  46766  fouriercn  46767  subsaliuncl  46893  gsumge0cl  46906  sge0tsms  46915  caragenuncllem  47047  0ome  47064  hoidmvle  47135  ovolval3  47182  ovolval4lem1  47184  smfpimbor1lem2  47334  gbpart7  48350  gbpart9  48352  gbpart11  48353  nnsum3primes4  48371  gpg5edgnedg  48713  xpiun  48741  lindslinindsimp2lem5  49045  ackval42a  49280  aacllem  50383