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

Theorem eqtr3i 2488
Description: An equality transitivity inference. (Contributed by NM, 6-May-1994.)
Hypotheses
Ref Expression
eqtr3i.1
eqtr3i.2
Assertion
Ref Expression
eqtr3i

Proof of Theorem eqtr3i
StepHypRef Expression
1 eqtr3i.1 . . 3
21eqcomi 2470 . 2
3 eqtr3i.2 . 2
42, 3eqtri 2486 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395
This theorem is referenced by:  3eqtr3i  2494  3eqtr3ri  2495  unundi  3664  unundir  3665  inindi  3714  inindir  3715  dfin4  3737  difun1  3757  difabs  3761  notab  3767  dif0  3898  difdifdir  3915  tpidm13  4132  tpprceq3  4170  intmin2  4314  univ  4703  iunxpconst  5061  dmres  5299  opabresid  5332  rnresi  5355  cnvcnv  5464  rnresv  5471  cnvsn0  5481  cnvsn  5496  resdmres  5503  coi2  5529  coires1  5530  dfdm2  5544  isarep2  5673  resasplit  5760  ssimaex  5938  fnreseql  5997  fnsuppeq0OLD  6132  resfunexg  6137  idref  6153  mpt2mpt  6394  caov31  6504  fvresex  6773  xpexgALT  6793  1st2val  6826  2nd2val  6827  fnsuppeq0  6947  ecopovtrn  7433  limensuci  7713  pssnn  7758  r1sucg  8208  jech9.3  8253  rankbnd2  8308  compss  8777  zorn2lem4  8900  iunfo  8935  cardf  8946  alephsuc3  8976  fpwwe2lem13  9041  rankcf  9176  halfnq  9375  addclprlem2  9416  mulgt0sr  9503  mul02lem2  9778  mul02  9779  addid1  9781  mvlladdi  9860  mvllmuli  10402  infmsup  10546  8th4div3  10784  nneo  10971  dec10  11034  nummac  11036  numadd  11038  numaddc  11039  nummul1c  11040  9p2e11  11066  decbin0  11107  rpsup  11993  resup  11994  om2uzrdg  12067  m1expcl2  12188  binom2aiOLD  12278  facnn  12355  fac0  12356  faclbnd4lem1  12371  hasheq0  12433  f1oun2prg  12865  sqrt1  13105  sqrt4  13106  sqrt9  13107  rddif  13173  abs3lemi  13242  sumss2  13548  geo2sum2  13683  geomulcvg  13685  geoihalfsum  13691  sin0  13884  efival  13887  ef01bndlem  13919  cos2bnd  13923  sin4lt0  13930  2prm  14233  unbenlem  14426  dec5dvds  14550  modxai  14554  mod2xi  14555  mod2xnegi  14557  gcdi  14559  numexp2x  14565  decsplit  14569  setsid  14673  mreexexlem3d  15043  oppchom  15110  2oppchomf  15119  isoval  15159  oppchofcl  15529  oyoncl  15539  mvdco  16470  m1expaddsub  16523  psgn0fv0  16536  oppglsm  16662  dprd2da  17091  ring1  17248  opprsubg  17285  lsppratlem1  17793  opsrtoslem1  18148  ply1basfvi  18282  coe1tm  18314  ply1coe  18337  ply1coeOLD  18338  zzngim  18591  cnmsgnsubg  18613  psgninv  18618  zrhpsgnmhm  18620  neitr  19681  comppfsc  20033  kgeni  20038  xkoinjcn  20188  ufprim  20410  metreslem  20865  restmetu  21090  retopbas  21267  cnfldms  21283  qdensere2  21302  xrsmopn  21317  metdscn2  21361  pcoass  21524  iscmet3lem3  21729  cncms  21795  cnfldcusp  21797  resscdrg  21798  rrxprds  21821  ovoliunnul  21918  uniioombllem4  21995  vitalilem5  22021  mbfres  22051  ismbf3d  22061  i1fima  22085  i1fd  22088  itg2cnlem1  22168  itgss3  22221  ellimc2  22281  limccnp2  22296  cpnres  22340  lhop  22417  plyeq0  22608  plypf1  22609  sinhalfpilem  22856  sincos6thpi  22908  sincos3rdpi  22909  pige3  22910  dfrelog  22953  logimul  22999  logneg2  23000  dvlog  23032  cxpsqrt  23084  ang180lem2  23142  ang180lem3  23143  ang180lem4  23144  quart1  23187  asin1  23225  atan0  23239  atanlogsublem  23246  atan1  23259  log2tlbnd  23276  log2ublem2  23278  log2ub  23280  basellem8  23361  cht2  23446  ppiub  23479  bposlem6  23564  bposlem8  23566  bposlem9  23567  lgsdir2lem3  23600  lgseisenlem1  23624  lgseisenlem2  23625  lgsquadlem1  23629  lgsquadlem2  23630  chebbnd1  23657  motplusg  23929  ax5seglem7  24238  ex-un  25145  circgrpOLD  25376  ipdirilem  25744  ipasslem10  25754  hisubcomi  26021  normlem0  26026  norm3difi  26064  norm3lem  26066  polid2i  26074  chdmj1i  26399  chjjdiri  26442  spansn0  26459  pjoml4i  26505  cmbr3i  26518  qlaxr3i  26554  honpcani  26744  honpncani  26746  lnopunilem1  26929  lnophmlem2  26936  lnfn0i  26961  pjbdlni  27068  pjclem1  27114  pjclem3  27116  pjci  27119  atomli  27301  atabs2i  27321  mddmdin0i  27350  difeq  27416  disjdifprg  27436  imadifxp  27458  fnresin  27470  ofpreima2  27508  df1stres  27522  df2ndres  27523  cnvoprab  27546  xrge0base  27673  xrge00  27674  xrge0mulgnn0  27677  xrge0slmod  27834  ordtconlem1  27906  xrge0iifcnv  27915  lmxrge0  27934  cnrrext  27991  esumpfinvallem  28080  measvuni  28185  measunl  28187  measinb  28192  mbfmcst  28230  sibfof  28282  eulerpartlemmf  28314  fib2  28341  fib3  28342  fib4  28343  fib5  28344  fib6  28345  0rrv  28390  coinfliprv  28421  ballotlem2  28427  ballotlemgun  28463  kur14lem6  28655  kur14lem7  28656  cvmlift2lem12  28759  problem5  29023  quad3  29024  4bc3eq4  29111  divcnvshft  29117  divcnvlin  29118  logi  29121  risefall0lem  29148  bpoly2  29819  bpoly3  29820  ptrest  30048  mblfinlem2  30052  ovoliunnfl  30056  voliunnfl  30058  itg2addnclem2  30067  ftc1anclem5  30094  ftc1anclem6  30095  sdc  30237  heiborlem3  30309  dnnumch1  30990  aomclem6  31005  areaquad  31184  seff  31189  sblpnf  31190  hashnzfz  31225  lhe4.4ex1a  31234  iccdifioo  31555  itgsin0pilem1  31748  stoweidlem13  31795  stoweidlem26  31808  fourierdlem62  31951  fourierdlem102  31991  fourierdlem114  32003  fourierswlem  32013  fouriersw  32014  estrres  32645  2zrngasgrp  32746  2zrngmsgrp  32753  mvlraddi  33180  mvlrmuli  33192  i2linesi  33193  bj-2upln1upl  34582  dvh4dimN  37174  unitadd  38016
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
  Copyright terms: Public domain W3C validator