Theorem eqtr2i 2787

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

Syntax hints:   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  3eqtrri  2791  3eqtr2ri  2793  dfun3  4229  dfif3  4502  dfsn2  4602  prprc1  4731  diftpsn3  4770  ssunpr  4799  sstp  4801  unidif0OLD  5331  xpindi  5819  xpindir  5820  dmcnvcnv  5923  rncnvcnv  5924  imainrect  6179  dfrn4  6201  imadifssran  6202  predres  6340  fcoi1  6752  foimacnv  6838  f1ossf1o  7124  fsnunfv  7185  difex2  7755  dfoprab3  8047  offval22  8079  suppvalbr  8156  fvmpocurryd  8263  mapsnconst  8886  sbthlem8  9078  fiint  9282  ordtypecbv  9475  trcl  9693  rankxplim2  9848  infdju1  10169  cfval2  10239  itunitc  10400  ituniiun  10401  hsmex2  10412  ltexnq  10955  ixi  11838  zeo  12677  num0h  12718  dec10p  12754  fseq1p1m1  13622  cats1fvn  14891  s3fn  14944  sgnneg  15133  fsumrelem  15855  ef0lem  16127  ef01bndlem  16235  sadcadd  16511  sadadd2  16513  3lcm2e6woprm  16668  mod2xnegi  17126  str0  17244  ressinbas  17300  mreexexlem4d  17698  0g0  18717  frmdplusg  18908  smndex1bas  18963  sgrp2nmndlem4  18985  sgrp2nmndlem5  18986  oppgplusfval  19413  symgsubmefmnd  19463  psgnsn  19585  psgnprfval1  19587  frgpnabllem1  19938  opprmulfval  20417  opprrngb  20424  opprringb  20426  opprunit  20455  isdrng3lem1  20851  00lsp  21102  rspvalint  21369  chrval  21673  dsmmelbas  21889  ltbwe  22195  ply1plusgfvi  22401  mat2pmatfval  22880  unisngl  23684  qtopres  23855  ufildr  24088  oppgtmd  24254  tgioo  24953  tgqioo  24957  dveflem  26138  lhop1lem  26172  sincos4thpi  26678  coskpi  26688  cxpsqrtlem  26867  log2ublem1  27111  efrlim  27134  basellem3  27247  bposlem9  27456  madeun  28077  precsexlem11  28410  graop  29379  0grsubgr  29628  usgrfilem  29677  finsumvtxdg2ssteplem4  29898  wlkvtxedg  29993  2wlkdlem1  30274  2pthd  30289  wlk2v2e  30508  3wlkdlem1  30510  3pthd  30525  konigsberg  30608  cnidOLD  30934  ip1ilem  31178  ipasslem10  31191  normlem6  31467  dfhnorm2  31474  h1de2i  31905  spansnji  31998  pjneli  32075  mayetes3i  32081  pjclem1  32547  mdslmd3i  32684  atabsi  32753  imadifxp  32946  dfdec100  33174  dpmul100  33216  dpmul1000  33218  dpmul4  33233  xrge00  33334  cyc2fv1  33441  cyc2fv2  33442  cyc3fv3  33459  opprlidlabs  33767  vieta  33970  cos9thpiminplylem5  34176  locfinref  34231  cnvordtrestixx  34303  raddcn  34319  rrhcn  34387  qqtopn  34401  esumpfinvallem  34464  sxbrsigalem1  34675  eulerpartgbij  34762  hgt750lem2  35039  subfacp1lem1  35671  subfacval2  35679  quad3  36162  ptrest  38270  poimirlem3  38274  poimirlem8  38279  poimirlem15  38286  mblfinlem3  38310  ismblfin  38312  areacirc  38364  pmapglb  40544  dvh4dimN  42221  hdmapfval  42601  12gcd5e1  42770  sqdeccom12  43050  remul02  43166  mapfzcons1  43448  lmhmlnmsplit  43814  pwssplit4  43816  clcnvlem  44349  cnvrcl0  44351  sqrtcval2  44368  resqrtvalex  44371  imsqrtvalex  44372  iunrelexp0  44428  sumnnodd  46346  climinf2mpt  46428  climinfmpt  46429  dvnmul  46657  wallispilem4  46782  dirkertrigeqlem3  46814  fourierdlem24  46845  fourierdlem57  46877  fourierdlem58  46878  fourierdlem80  46900  fourierswlem  46944  fouriersw  46945  fouriercn  46946  subsaliuncl  47072  gsumge0cl  47085  sge0tsms  47094  caragenuncllem  47226  0ome  47243  hoidmvle  47314  ovolval3  47361  ovolval4lem1  47363  smfpimbor1lem2  47513  gbpart7  48532  gbpart9  48534  gbpart11  48535  nnsum3primes4  48553  gpg5edgnedg  48895  xpiun  48923  lindslinindsimp2lem5  49242  ackval42a  49477  aacllem  50621