Theorem eqtr2i 2769

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 2768	. 2 ⊢ 𝐴 = 𝐶
4	3	eqcomi 2749	1 ⊢ 𝐶 = 𝐴

Syntax hints:   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  3eqtrri  2773  3eqtr2ri  2775  dfun3  4295  dfif3  4562  dfsn2  4661  prprc1  4790  diftpsn3  4827  ssunpr  4859  sstp  4861  unidif0  5378  xpindi  5858  xpindir  5859  dmcnvcnv  5958  rncnvcnv  5959  imainrect  6212  dfrn4  6233  predres  6371  fcoi1  6795  foimacnv  6879  f1ossf1o  7162  fsnunfv  7221  difex2  7795  dfoprab3  8095  offval22  8129  suppvalbr  8205  fvmpocurryd  8312  mapsnconst  8950  sbthlem8  9156  fiint  9394  fiintOLD  9395  ordtypecbv  9586  trcl  9797  rankxplim2  9949  infdju1  10259  cfval2  10329  itunitc  10490  ituniiun  10491  hsmex2  10502  ltexnq  11044  ixi  11919  zeo  12729  num0h  12770  dec10p  12801  fseq1p1m1  13658  cats1fvn  14907  s3fn  14960  fsumrelem  15855  ef0lem  16126  ef01bndlem  16232  sadcadd  16504  sadadd2  16506  3lcm2e6woprm  16662  mod2xnegi  17118  decexp2  17122  str0  17236  ressinbas  17304  mreexexlem4d  17705  0g0  18702  frmdplusg  18889  smndex1bas  18941  sgrp2nmndlem4  18963  sgrp2nmndlem5  18964  oppgplusfval  19388  symgsubmefmnd  19440  psgnsn  19562  psgnprfval1  19564  frgpnabllem1  19915  opprmulfval  20362  opprrngb  20372  opprringb  20374  opprunit  20403  00lsp  21002  chrval  21561  dsmmelbas  21782  ltbwe  22085  ply1plusgfvi  22264  mat2pmatfval  22750  unisngl  23556  qtopres  23727  ufildr  23960  oppgtmd  24126  tgioo  24837  tgqioo  24841  dveflem  26037  lhop1lem  26072  sincos4thpi  26573  coskpi  26583  cxpsqrtlem  26762  log2ublem1  27007  efrlim  27030  efrlimOLD  27031  basellem3  27144  bposlem9  27354  madeun  27940  precsexlem11  28259  0reno  28447  graop  29064  0grsubgr  29313  usgrfilem  29362  finsumvtxdg2ssteplem4  29584  wlkvtxedg  29680  2wlkdlem1  29958  2pthd  29973  wlk2v2e  30189  3wlkdlem1  30191  3pthd  30206  konigsberg  30289  cnidOLD  30614  ip1ilem  30858  ipasslem10  30871  normlem6  31147  dfhnorm2  31154  h1de2i  31585  spansnji  31678  pjneli  31755  mayetes3i  31761  pjclem1  32227  mdslmd3i  32364  atabsi  32433  imadifxp  32623  dfdec100  32834  dpmul100  32861  dpmul1000  32863  dpmul4  32878  xrge00  32998  cyc2fv1  33114  cyc2fv2  33115  cyc3fv3  33132  opprlidlabs  33478  locfinref  33787  cnvordtrestixx  33859  raddcn  33875  rrhcn  33943  qqtopn  33957  esumpfinvallem  34038  sxbrsigalem1  34250  eulerpartgbij  34337  sgnneg  34505  hgt750lem2  34629  subfacp1lem1  35147  subfacval2  35155  quad3  35638  ptrest  37579  poimirlem3  37583  poimirlem8  37588  poimirlem15  37595  mblfinlem3  37619  ismblfin  37621  areacirc  37673  pmapglb  39727  dvh4dimN  41404  hdmapfval  41784  12gcd5e1  41960  sqdeccom12  42278  remul02  42381  mapfzcons1  42673  lmhmlnmsplit  43044  pwssplit4  43046  clcnvlem  43585  cnvrcl0  43587  sqrtcval2  43604  resqrtvalex  43607  imsqrtvalex  43608  iunrelexp0  43664  sumnnodd  45551  climinf2mpt  45635  climinfmpt  45636  dvnmul  45864  wallispilem4  45989  dirkertrigeqlem3  46021  fourierdlem24  46052  fourierdlem57  46084  fourierdlem58  46085  fourierdlem80  46107  fourierswlem  46151  fouriersw  46152  fouriercn  46153  subsaliuncl  46279  gsumge0cl  46292  sge0tsms  46301  caragenuncllem  46433  0ome  46450  hoidmvle  46521  ovolval3  46568  ovolval4lem1  46570  smfpimbor1lem2  46720  gbpart7  47641  gbpart9  47643  gbpart11  47644  nnsum3primes4  47662  xpiun  47881  lindslinindsimp2lem5  48191  ackval42a  48431  aacllem  48895