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

Theorem eqtr2i 2304
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 2303 . 2  |-  A  =  C
43eqcomi 2287 1  |-  C  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1623
This theorem is referenced by:  3eqtrri  2308  3eqtr2ri  2310  dfun3  3407  symdif1  3433  dfif3  3575  dfsn2  3654  prprc1  3736  ssunpr  3776  sstp  3778  unidif0  4183  pwundif  4300  difex2  4525  xpindi  4819  xpindir  4820  dmcnvcnv  4901  rncnvcnv  4902  imainrect  5119  dfrn4  5134  fcoi1  5415  foimacnv  5490  fsnunfv  5720  dfoprab3  6176  mapsnconst  6813  sbthlem8  6978  fiint  7133  ordtypecbv  7232  ruv  7314  cantnf  7395  trcl  7410  rankxplim2  7550  infcda1  7819  cfval2  7886  itunitc  8047  ituniiun  8048  hsmex2  8059  ltexnq  8599  ixi  9397  zeo  10097  num0h  10134  dec10p  10153  fseq1p1m1  10857  cats1fvn  11508  fsumrelem  12265  ef0lem  12360  ef01bndlem  12464  sadcadd  12649  sadadd2  12651  mod2xnegi  13086  decexp2  13090  str0  13184  ressinbas  13204  mreexexlem4d  13549  0g0  14386  frmdplusg  14476  oppgplusfval  14821  frgpnabllem1  15161  opprmulfval  15407  opprrngb  15414  opprunit  15443  00lsp  15738  psrmulr  16129  ltbwe  16214  ply1plusgfvi  16320  chrval  16479  qtopres  17389  ufildr  17626  oppgtmd  17780  tgioo  18302  tgqioo  18306  dveflem  19326  lhop1lem  19360  sincos4thpi  19881  coskpi  19888  cxpsqrlem  20049  log2ublem1  20242  efrlim  20264  basellem3  20320  bposlem9  20531  cnid  21018  ip1ilem  21404  ipasslem10  21417  normlem6  21694  dfhnorm2  21701  h1de2i  22132  spansnji  22225  pjneli  22302  mayetes3i  22309  lnophmlem2  22597  pjclem1  22775  mdslmd3i  22912  atabsi  22981  pwundif2  23186  xppreima  23211  cnvordtrestixx  23297  raddcn  23302  xrge00  23311  esumpfinvallem  23442  isrnsigaOLD  23473  subfacp1lem1  23710  subfacval2  23718  ghomsn  23995  areacirc  24931  nZdef  25180  1cat  25759  selsubf  25990  mapfzcons1  26794  lmhmlnmsplit  27185  pwssplit4  27191  dsmmelbas  27205  wallispilem4  27817  pmapglb  29959  dvh4dimN  31637  hdmapfval  32020
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator