MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqtr2i Unicode version

Theorem eqtr2i 2379
Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.)
Hypotheses
Ref Expression
eqtr2i.1  |-  A  =  B
eqtr2i.2  |-  B  =  C
Assertion
Ref Expression
eqtr2i  |-  C  =  A

Proof of Theorem eqtr2i
StepHypRef Expression
1 eqtr2i.1 . . 3  |-  A  =  B
2 eqtr2i.2 . . 3  |-  B  =  C
31, 2eqtri 2378 . 2  |-  A  =  C
43eqcomi 2362 1  |-  C  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1642
This theorem is referenced by:  3eqtrri  2383  3eqtr2ri  2385  dfun3  3483  symdif1  3509  dfif3  3651  dfsn2  3730  prprc1  3812  ssunpr  3855  sstp  3857  unidif0  4262  pwundif  4379  difex2  4604  xpindi  4898  xpindir  4899  dmcnvcnv  4980  rncnvcnv  4981  imainrect  5198  dfrn4  5213  fcoi1  5495  foimacnv  5570  fsnunfv  5801  dfoprab3  6260  mapsnconst  6898  sbthlem8  7063  fiint  7220  ordtypecbv  7319  ruv  7401  cantnf  7482  trcl  7497  rankxplim2  7637  infcda1  7906  cfval2  7973  itunitc  8134  ituniiun  8135  hsmex2  8146  ltexnq  8686  ixi  9484  zeo  10186  num0h  10223  dec10p  10242  fseq1p1m1  10946  cats1fvn  11598  fsumrelem  12356  ef0lem  12451  ef01bndlem  12555  sadcadd  12740  sadadd2  12742  mod2xnegi  13177  decexp2  13181  str0  13275  ressinbas  13295  mreexexlem4d  13642  0g0  14479  frmdplusg  14569  oppgplusfval  14914  frgpnabllem1  15254  opprmulfval  15500  opprrngb  15507  opprunit  15536  00lsp  15831  psrmulr  16222  ltbwe  16307  ply1plusgfvi  16413  chrval  16579  qtopres  17489  ufildr  17722  oppgtmd  17876  tgioo  18398  tgqioo  18402  dveflem  19424  lhop1lem  19458  sincos4thpi  19982  coskpi  19989  cxpsqrlem  20154  log2ublem1  20347  efrlim  20369  basellem3  20426  bposlem9  20637  cnid  21124  ip1ilem  21512  ipasslem10  21525  normlem6  21802  dfhnorm2  21809  h1de2i  22240  spansnji  22333  pjneli  22410  mayetes3i  22417  lnophmlem2  22705  pjclem1  22883  mdslmd3i  23020  atabsi  23089  pwundif2  23194  imadifxp  23238  xppreima  23259  xrge00  23400  cnvordtrestixx  23467  raddcn  23471  esumpfinvallem  23730  isrnsigaOLD  23761  subfacp1lem1  24114  subfacval2  24122  ghomsn  24399  areacirc  25523  mapfzcons1  26117  lmhmlnmsplit  26508  pwssplit4  26514  dsmmelbas  26528  wallispilem4  27140  wlkntrllem4  27687  pmapglb  30011  dvh4dimN  31689  hdmapfval  32072
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2351
  Copyright terms: Public domain W3C validator