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

Theorem eqtr3i 2633
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 2618 . 2 𝐵 = 𝐴
3 eqtr3i.2 . 2 𝐴 = 𝐶
42, 3eqtri 2631 1 𝐵 = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602
This theorem is referenced by:  3eqtr3i  2639  3eqtr3ri  2640  unundi  3735  unundir  3736  inindi  3791  inindir  3792  dfin4  3825  difun1  3845  difabs  3850  notab  3855  dif0  3903  difdifdir  4007  tpidm13  4234  intmin2  4433  iunxdif3  4536  univ  4840  iunxpconst  5088  dmres  5326  opabresid  5361  rnresi  5385  cnvcnv  5491  rnresv  5498  cnvsn0  5507  cnvsn  5522  resdmres  5529  coi2  5555  coires1  5556  dfdm2  5570  isarep2  5878  resasplit  5972  ssimaex  6158  fnreseql  6220  resfunexg  6362  idref  6381  mpt2mpt  6628  caov31  6738  fvresex  7009  xpexgALT  7029  1st2val  7062  2nd2val  7063  fnsuppeq0  7187  ecopovtrn  7714  limensuci  7998  pssnn  8040  r1sucg  8492  jech9.3  8537  rankbnd2  8592  compss  9058  zorn2lem4  9181  iunfo  9217  cardf  9228  alephsuc3  9258  fpwwe2lem13  9320  rankcf  9455  halfnq  9654  addclprlem2  9695  mulgt0sr  9782  mul02lem2  10064  mul02  10065  addid1  10067  mvlladdi  10150  mvllmuli  10707  infrenegsup  10853  8th4div3  11099  nneo  11293  dec10OLD  11387  nummac  11390  numadd  11392  numaddc  11393  nummul1c  11394  9p2e11OLD  11452  decbin0  11514  rpsup  12482  resup  12483  om2uzrdg  12572  m1expcl2  12699  facnn  12879  fac0  12880  faclbnd4lem1  12897  4bc3eq4  12932  hasheq0  12967  f1oun2prg  13458  sqrt1  13806  sqrt4  13807  sqrt9  13808  rddif  13874  abs3lemi  13943  sumss2  14250  divcnvshft  14372  geo2sum2  14390  geomulcvg  14392  geoihalfsum  14399  risefall0lem  14542  bpoly2  14573  bpoly3  14574  sin0  14664  efival  14667  ef01bndlem  14699  cos2bnd  14703  sin4lt0  14710  flodddiv4  14921  2prm  15189  unbenlem  15396  dec5dvds  15552  modxai  15556  mod2xi  15557  mod2xnegi  15559  gcdi  15561  numexp2x  15567  decsplit  15571  decsplitOLD  15575  setsid  15688  mreexexlem3d  16075  oppchom  16144  2oppchomf  16153  isoval  16194  estrres  16548  oppchofcl  16669  oyoncl  16679  mvdco  17634  m1expaddsub  17687  psgn0fv0  17700  oppglsm  17826  dprd2da  18210  ring1  18371  opprsubg  18405  lsppratlem1  18914  opsrtoslem1  19251  ply1basfvi  19378  coe1tm  19410  ply1coe  19433  zzngim  19665  cnmsgnsubg  19687  psgninv  19692  zrhpsgnmhm  19694  neitr  20736  comppfsc  21087  kgeni  21092  xkoinjcn  21242  ufprim  21465  metreslem  21918  restmetu  22126  retopbas  22306  cnfldms  22321  qdensere2  22340  xrsmopn  22355  metdscn2  22399  pcoass  22563  iscmet3lem3  22814  cncms  22876  cnfldcusp  22878  resscdrg  22879  rrxprds  22902  ovoliunnul  22999  uniioombllem4  23077  vitalilem5  23104  mbfres  23134  ismbf3d  23144  i1fima  23168  i1fd  23171  itg2cnlem1  23251  itgss3  23304  ellimc2  23364  limccnp2  23379  cpnres  23423  lhop  23500  plyeq0  23688  plypf1  23689  sinhalfpilem  23936  sincos6thpi  23988  sincos3rdpi  23989  pige3  23990  dfrelog  24033  logimul  24081  logneg2  24082  dvlog  24114  cxpsqrt  24166  ang180lem2  24257  ang180lem3  24258  ang180lem4  24259  quart1  24300  asin1  24338  atan0  24352  atanlogsublem  24359  atan1  24372  log2tlbnd  24389  log2ublem2  24391  log2ub  24393  basellem8  24531  cht2  24615  ppiub  24646  bposlem6  24731  bposlem8  24733  bposlem9  24734  lgsdir2lem3  24769  lgseisenlem1  24817  lgseisenlem2  24818  lgsquadlem1  24822  lgsquadlem2  24823  2lgsoddprmlem2  24851  chebbnd1  24878  istrkg3ld  25077  tgcgr4  25144  motplusg  25155  ax5seglem7  25533  ex-un  26439  ex-sqrt  26469  ipdirilem  26874  ipasslem10  26884  hisubcomi  27151  normlem0  27156  norm3difi  27194  norm3lem  27196  polid2i  27204  chdmj1i  27530  chjjdiri  27573  spansn0  27590  pjoml4i  27636  cmbr3i  27649  qlaxr3i  27685  honpcani  27874  honpncani  27876  lnopunilem1  28059  lnophmlem2  28066  lnfn0i  28091  pjbdlni  28198  pjclem1  28244  pjclem3  28246  pjci  28249  atomli  28431  atabs2i  28451  mddmdin0i  28480  difeq  28545  disjdifprg  28576  imadifxp  28602  fnresin  28618  ofpreima2  28655  df1stres  28670  df2ndres  28671  cnvoprab  28692  xrge0base  28822  xrge00  28823  xrge0mulgnn0  28826  xrge0slmod  28981  lmatfvlem  29015  xrge0iifcnv  29113  lmxrge0  29132  cnrrext  29188  qqtopn  29189  esumrnmpt2  29263  esumpfinvallem  29269  unelldsys  29354  ldgenpisyslem1  29359  measunl  29412  mbfmcst  29454  difelcarsg  29505  carsggect  29513  sibfof  29535  eulerpartlemmf  29570  fib2  29597  fib3  29598  fib4  29599  fib5  29600  fib6  29601  0rrv  29646  coinfliprv  29677  ballotlem2  29683  kur14lem6  30253  kur14lem7  30254  cvmlift2lem12  30356  problem5  30623  quad3  30624  divcnvlin  30677  logi  30679  bj-2upln1upl  32001  bj-rest0  32023  relowlssretop  32183  relowlpssretop  32184  1oequni2o  32188  curunc  32357  ptrest  32374  poimirlem16  32391  poimirlem30  32405  mblfinlem2  32413  ovoliunnfl  32417  voliunnfl  32419  itg2addnclem2  32428  ftc1anclem5  32455  ftc1anclem6  32456  sdc  32506  heiborlem3  32578  dvh4dimN  35550  dnnumch1  36428  aomclem6  36443  areaquad  36617  unitadd  37316  seff  37326  sblpnf  37327  hashnzfz  37337  lhe4.4ex1a  37346  iccdifioo  38385  itgsin0pilem1  38638  stoweidlem13  38703  stoweidlem26  38716  fourierdlem62  38858  fourierdlem102  38898  fourierdlem114  38910  fourierswlem  38920  fouriersw  38921  sge0tsms  39070  meaiuninc  39171  fmtno4prmfac  39820  41prothprm  39872  2zrngasgrp  41725  2zrngmsgrp  41732  mvlraddi  42279  mvlrmuli  42288  i2linesi  42289
  Copyright terms: Public domain W3C validator