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

Theorem eqtr3i 2485
Description: An equality transitivity inference. (Contributed by NM, 6-May-1994.)
Hypotheses
Ref Expression
eqtr3i.1  |-  A  =  B
eqtr3i.2  |-  A  =  C
Assertion
Ref Expression
eqtr3i  |-  B  =  C

Proof of Theorem eqtr3i
StepHypRef Expression
1 eqtr3i.1 . . 3  |-  A  =  B
21eqcomi 2470 . 2  |-  B  =  A
3 eqtr3i.2 . 2  |-  A  =  C
42, 3eqtri 2483 1  |-  B  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-cleq 2454
This theorem is referenced by:  3eqtr3i  2491  3eqtr3ri  2492  unundi  3606  unundir  3607  inindi  3660  inindir  3661  dfin4  3694  difun1  3714  difabs  3718  notab  3724  dif0  3848  difdifdir  3866  tpidm13  4086  tpprceq3  4124  intmin2  4275  univ  4664  iunxpconst  4909  dmres  5143  opabresid  5176  rnresi  5199  cnvcnv  5306  rnresv  5313  cnvsn0  5322  cnvsn  5337  resdmres  5344  coi2  5370  coires1  5371  dfdm2  5386  isarep2  5684  resasplit  5775  ssimaex  5952  fnreseql  6014  resfunexg  6154  idref  6170  mpt2mpt  6414  caov31  6524  fvresex  6792  xpexgALT  6812  1st2val  6845  2nd2val  6846  fnsuppeq0  6969  ecopovtrn  7491  limensuci  7773  pssnn  7815  r1sucg  8265  jech9.3  8310  rankbnd2  8365  compss  8831  zorn2lem4  8954  iunfo  8989  cardf  9000  alephsuc3  9030  fpwwe2lem13  9092  rankcf  9227  halfnq  9426  addclprlem2  9467  mulgt0sr  9554  mul02lem2  9835  mul02  9836  addid1  9838  mvlladdi  9917  mvllmuli  10467  infrenegsup  10618  infmsupOLD  10619  8th4div3  10861  nneo  11047  dec10  11109  nummac  11111  numadd  11113  numaddc  11114  nummul1c  11115  9p2e11  11141  decbin0  11182  rpsup  12124  resup  12125  om2uzrdg  12201  m1expcl2  12325  facnn  12492  fac0  12493  faclbnd4lem1  12509  4bc3eq4  12544  hasheq0  12575  f1oun2prg  13047  sqrt1  13383  sqrt4  13384  sqrt9  13385  rddif  13451  abs3lemi  13520  sumss2  13840  divcnvshft  13961  geo2sum2  13978  geomulcvg  13980  geoihalfsum  13986  risefall0lem  14127  bpoly2  14158  bpoly3  14159  sin0  14251  efival  14254  ef01bndlem  14286  cos2bnd  14290  sin4lt0  14297  2prm  14688  unbenlem  14900  dec5dvds  15084  modxai  15088  mod2xi  15089  mod2xnegi  15091  gcdi  15093  numexp2x  15099  decsplit  15103  setsid  15212  mreexexlem3d  15600  oppchom  15668  2oppchomf  15677  isoval  15718  estrres  16072  oppchofcl  16193  oyoncl  16203  mvdco  17134  m1expaddsub  17187  psgn0fv0  17200  oppglsm  17342  dprd2da  17723  ring1  17878  opprsubg  17912  lsppratlem1  18418  opsrtoslem1  18755  ply1basfvi  18882  coe1tm  18914  ply1coe  18937  ply1coeOLD  18938  zzngim  19171  cnmsgnsubg  19193  psgninv  19198  zrhpsgnmhm  19200  neitr  20244  comppfsc  20595  kgeni  20600  xkoinjcn  20750  ufprim  20972  metreslem  21425  restmetu  21633  retopbas  21829  cnfldms  21844  qdensere2  21863  xrsmopn  21878  metdscn2  21922  metdscn2OLD  21937  pcoass  22103  iscmet3lem3  22308  cncms  22370  cnfldcusp  22372  resscdrg  22373  rrxprds  22396  ovoliunnul  22508  uniioombllem4  22592  vitalilem5  22618  mbfres  22648  ismbf3d  22658  i1fima  22684  i1fd  22687  itg2cnlem1  22767  itgss3  22820  ellimc2  22880  limccnp2  22895  cpnres  22939  lhop  23016  plyeq0  23213  plypf1  23214  sinhalfpilem  23466  sincos6thpi  23518  sincos3rdpi  23519  pige3  23520  dfrelog  23563  logimul  23611  logneg2  23612  dvlog  23644  cxpsqrt  23696  ang180lem2  23787  ang180lem3  23788  ang180lem4  23789  quart1  23830  asin1  23868  atan0  23882  atanlogsublem  23889  atan1  23902  log2tlbnd  23919  log2ublem2  23921  log2ub  23923  basellem8  24062  cht2  24147  ppiub  24180  bposlem6  24265  bposlem8  24267  bposlem9  24268  lgsdir2lem3  24301  lgseisenlem1  24325  lgseisenlem2  24326  lgsquadlem1  24330  lgsquadlem2  24331  chebbnd1  24358  istrkg3ld  24557  tgcgr4  24624  motplusg  24635  ax5seglem7  25013  ex-un  25922  circgrpOLD  26150  ipdirilem  26518  ipasslem10  26528  hisubcomi  26805  normlem0  26810  norm3difi  26848  norm3lem  26850  polid2i  26858  chdmj1i  27182  chjjdiri  27225  spansn0  27242  pjoml4i  27288  cmbr3i  27301  qlaxr3i  27337  honpcani  27526  honpncani  27528  lnopunilem1  27711  lnophmlem2  27718  lnfn0i  27743  pjbdlni  27850  pjclem1  27896  pjclem3  27898  pjci  27901  atomli  28083  atabs2i  28103  mddmdin0i  28132  difeq  28199  iunxdif3  28223  disjdifprg  28233  imadifxp  28260  fnresin  28276  ofpreima2  28317  df1stres  28332  df2ndres  28333  cnvoprab  28356  xrge0base  28495  xrge00  28496  xrge0mulgnn0  28499  xrge0slmod  28655  lmatfvlem  28689  ordtconlem1  28778  xrge0iifcnv  28787  lmxrge0  28806  cnrrext  28862  qqtopn  28863  esumrnmpt2  28937  esumpfinvallem  28943  unelldsys  29028  ldgenpisyslem1  29033  measvuni  29084  measunl  29086  measinb  29091  mbfmcst  29129  difelcarsg  29190  carsggect  29198  sibfof  29221  eulerpartlemmf  29256  fib2  29283  fib3  29284  fib4  29285  fib5  29286  fib6  29287  0rrv  29332  coinfliprv  29363  ballotlem2  29369  ballotlemgun  29405  ballotlemgunOLD  29443  kur14lem6  29982  kur14lem7  29983  cvmlift2lem12  30085  problem5  30349  quad3  30350  divcnvlin  30415  logi  30418  bj-2upln1upl  31662  relowlssretop  31810  relowlpssretop  31811  1oequni2o  31815  ptrest  31983  poimirlem16  32000  poimirlem30  32014  mblfinlem2  32022  ovoliunnfl  32026  voliunnfl  32028  itg2addnclem2  32038  ftc1anclem5  32065  ftc1anclem6  32066  sdc  32117  heiborlem3  32189  dvh4dimN  35059  dnnumch1  35946  aomclem6  35961  areaquad  36145  unitadd  36685  seff  36700  sblpnf  36701  hashnzfz  36712  lhe4.4ex1a  36721  iccdifioo  37653  itgsin0pilem1  37863  stoweidlem13  37910  stoweidlem26  37923  fourierdlem62  38069  fourierdlem102  38109  fourierdlem114  38121  fourierswlem  38131  fouriersw  38132  sge0tsms  38259  41prothprm  38956  2zrngasgrp  40212  2zrngmsgrp  40219  mvlraddi  40776  mvlrmuli  40788  i2linesi  40789
  Copyright terms: Public domain W3C validator