Theorem eqtr2i 2487

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 2486	. 2
4	3	eqcomi 2470	1

Syntax hints:  =wceq 1395

This theorem is referenced by:  3eqtrri  2491  3eqtr2ri  2493  dfun3  3735  symdif1  3762  dfif3  3955  dfsn2  4042  prprc1  4140  ssunpr  4192  sstp  4194  unidif0  4625  pwundif  4792  xpindi  5141  xpindir  5142  dmcnvcnv  5230  rncnvcnv  5231  imainrect  5453  dfrn4  5472  fcoi1  5764  foimacnv  5838  fsnunfv  6111  difex2  6607  dfoprab3  6856  offval22  6879  fvmpt2curryd  7019  mapsnconst  7484  sbthlem8  7654  fiint  7817  ordtypecbv  7963  ruv  8048  cantnfOLD  8155  trcl  8180  rankxplim2  8319  infcda1  8594  cfval2  8661  itunitc  8822  ituniiun  8823  hsmex2  8834  ltexnq  9374  ixi  10203  zeo  10973  num0h  11014  dec10p  11033  fseq1p1m1  11781  cats1fvn  12823  fsumrelem  13621  ef0lem  13814  ef01bndlem  13919  sadcadd  14108  sadadd2  14110  mod2xnegi  14557  decexp2  14561  str0  14670  ressinbas  14693  mreexexlem4d  15044  0g0  15890  frmdplusg  16022  sgrp2nmndlem4  16046  sgrp2nmndlem5  16047  oppgplusfval  16383  psgnsn  16545  psgnprfval1  16547  frgpnabllem1  16877  opprmulfval  17274  opprringb  17281  opprunit  17310  00lsp  17627  psrmulr  18037  ltbwe  18137  ply1plusgfvi  18283  chrval  18562  dsmmelbas  18770  mat2pmatfval  19224  unisngl  20028  qtopres  20199  ufildr  20432  oppgtmd  20596  tgioo  21301  tgqioo  21305  dveflem  22380  lhop1lem  22414  sincos4thpi  22906  coskpi  22913  cxpsqrtlem  23083  log2ublem1  23277  efrlim  23299  basellem3  23356  bposlem9  23567  wlkntrllem2  24562  cnid  25353  ip1ilem  25741  ipasslem10  25754  normlem6  26032  dfhnorm2  26039  h1de2i  26471  spansnji  26564  pjneli  26641  mayetes3i  26648  pjclem1  27114  mdslmd3i  27251  atabsi  27320  imadifxp  27458  xrge00  27674  locfinref  27844  cnvordtrestixx  27895  raddcn  27911  rrhcn  27978  esumpfinvallem  28080  isrnsigaOLD  28112  sxbrsigalem1  28256  eulerpartgbij  28311  sgnneg  28479  subfacp1lem1  28623  subfacval2  28631  quad3  29024  ghomsn  29028  ptrest  30048  mblfinlem3  30053  ismblfin  30055  areacirc  30112  mapfzcons1  30649  lmhmlnmsplit  31033  pwssplit4  31035  sumnnodd  31636  dvnmul  31740  wallispilem4  31850  dirkertrigeqlem3  31882  fourierdlem24  31913  fourierdlem57  31946  fourierdlem58  31947  fourierdlem80  31969  fourierswlem  32013  fouriersw  32014  fouriercn  32015  usgfis  32446  xpiun  32454  lindslinindsimp2lem5  33063  aacllem  33216  pmapglb  35494  dvh4dimN  37174  hdmapfval  37557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-cleq 2449