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

Theorem eqtr3i 2644
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 2629 . 2 𝐵 = 𝐴
3 eqtr3i.2 . 2 𝐴 = 𝐶
42, 3eqtri 2642 1 𝐵 = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613
This theorem is referenced by:  3eqtr3i  2650  3eqtr3ri  2651  unundi  3766  unundir  3767  inindi  3822  inindir  3823  dfin4  3859  difun1  3879  difabs  3884  notab  3889  dif0  3941  difdifdir  4047  tpidm13  4282  intmin2  4495  iunxdif3  4597  univ  4910  iunxpconst  5165  dmres  5407  opabresid  5443  rnresi  5467  cnvcnvOLD  5575  rnresv  5582  cnvsn0  5591  cnvsn  5606  resdmres  5613  coi2  5640  coires1  5641  dfdm2  5655  isarep2  5966  resasplit  6061  ssimaex  6250  fnreseql  6313  resfunexg  6464  idref  6484  mpt2mpt  6737  caov31  6848  fvresex  7124  xpexgALT  7146  1st2val  7179  2nd2val  7180  fnsuppeq0  7308  ecopovtrn  7835  limensuci  8121  pssnn  8163  r1sucg  8617  jech9.3  8662  rankbnd2  8717  compss  9183  zorn2lem4  9306  iunfo  9346  cardf  9357  alephsuc3  9387  fpwwe2lem13  9449  rankcf  9584  halfnq  9783  addclprlem2  9824  mulgt0sr  9911  mul02lem2  10198  mul02  10199  addid1  10201  mvlladdi  10284  mvllmuli  10843  infrenegsup  10991  8th4div3  11237  nneo  11446  dec10OLD  11540  nummac  11543  numadd  11545  numaddc  11546  nummul1c  11547  9p2e11OLD  11605  decbin0  11667  rpsup  12648  resup  12649  om2uzrdg  12738  m1expcl2  12865  facnn  13045  fac0  13046  faclbnd4lem1  13063  4bc3eq4  13098  hasheq0  13137  f1oun2prg  13643  sqrt1  13993  sqrt4  13994  sqrt9  13995  rddif  14061  abs3lemi  14130  sumss2  14438  divcnvshft  14568  geo2sum2  14586  geomulcvg  14588  geoihalfsum  14595  risefall0lem  14738  bpoly2  14769  bpoly3  14770  sin0  14860  efival  14863  ef01bndlem  14895  cos2bnd  14899  sin4lt0  14906  flodddiv4  15118  2prm  15386  unbenlem  15593  dec5dvds  15749  modxai  15753  mod2xi  15754  mod2xnegi  15756  gcdi  15758  numexp2x  15764  decsplit  15768  decsplitOLD  15772  setsid  15895  mreexexlem3d  16287  oppchom  16356  2oppchomf  16365  isoval  16406  estrres  16760  oppchofcl  16881  oyoncl  16891  mvdco  17846  m1expaddsub  17899  psgn0fv0  17912  oppglsm  18038  dprd2da  18422  ring1  18583  opprsubg  18617  lsppratlem1  19128  opsrtoslem1  19465  ply1basfvi  19592  coe1tm  19624  ply1coe  19647  zzngim  19882  cnmsgnsubg  19904  psgninv  19909  zrhpsgnmhm  19911  neitr  20965  comppfsc  21316  kgeni  21321  xkoinjcn  21471  ufprim  21694  metreslem  22148  restmetu  22356  retopbas  22545  cnfldms  22560  qdensere2  22581  xrsmopn  22596  metdscn2  22641  pcoass  22805  recvs  22927  zclmncvs  22929  iscmet3lem3  23069  cncms  23132  cnfldcusp  23134  resscdrg  23135  rrxprds  23158  ovoliunnul  23256  uniioombllem4  23335  vitalilem5  23362  mbfres  23392  ismbf3d  23402  i1fima  23426  i1fd  23429  itg2cnlem1  23509  itgss3  23562  ellimc2  23622  limccnp2  23637  cpnres  23681  lhop  23760  plyeq0  23948  plypf1  23949  sinhalfpilem  24196  sincos6thpi  24248  sincos3rdpi  24249  pige3  24250  dfrelog  24293  logimul  24341  logneg2  24342  dvlog  24378  cxpsqrt  24430  ang180lem2  24521  ang180lem3  24522  ang180lem4  24523  quart1  24564  asin1  24602  atan0  24616  atanlogsublem  24623  atan1  24636  log2tlbnd  24653  log2ublem2  24655  log2ub  24657  basellem8  24795  cht2  24879  ppiub  24910  bposlem6  24995  bposlem8  24997  bposlem9  24998  lgsdir2lem3  25033  lgseisenlem1  25081  lgseisenlem2  25082  lgsquadlem1  25086  lgsquadlem2  25087  2lgsoddprmlem2  25115  chebbnd1  25142  istrkg3ld  25341  tgcgr4  25407  motplusg  25418  ax5seglem7  25796  ex-un  27251  ex-sqrt  27281  ipdirilem  27654  ipasslem10  27664  hisubcomi  27931  normlem0  27936  norm3difi  27974  norm3lem  27976  polid2i  27984  chdmj1i  28310  chjjdiri  28353  spansn0  28370  pjoml4i  28416  cmbr3i  28429  qlaxr3i  28465  honpcani  28654  honpncani  28656  lnopunilem1  28839  lnophmlem2  28846  lnfn0i  28871  pjbdlni  28978  pjclem1  29024  pjclem3  29026  pjci  29029  atomli  29211  atabs2i  29231  mddmdin0i  29260  difeq  29327  disjdifprg  29360  imadifxp  29386  fnresin  29403  ofpreima2  29440  df1stres  29455  df2ndres  29456  cnvoprab  29472  dfdec100  29550  decdiv10  29578  dpmul100  29579  dpmul1000  29581  dpexpp1  29590  dpadd2  29592  dpadd  29593  dpmul  29595  dpmul4  29596  threehalves  29597  xrge0base  29659  xrge00  29660  xrge0mulgnn0  29663  xrge0slmod  29818  lmatfvlem  29855  xrge0iifcnv  29953  lmxrge0  29972  cnrrext  30028  qqtopn  30029  esumrnmpt2  30104  esumpfinvallem  30110  unelldsys  30195  ldgenpisyslem1  30200  measunl  30253  mbfmcst  30295  difelcarsg  30346  carsggect  30354  sibfof  30376  eulerpartlemmf  30411  fib2  30438  fib3  30439  fib4  30440  fib5  30441  fib6  30442  0rrv  30487  coinfliprv  30518  ballotlem2  30524  prodfzo03  30655  chtvalz  30681  hgt750lemd  30700  hgt750lem  30703  hgt750lem2  30704  kur14lem6  31167  kur14lem7  31168  cvmlift2lem12  31270  problem5  31537  quad3  31538  divcnvlin  31593  logi  31595  bj-2upln1upl  32987  bj-rest0  33021  relowlssretop  33182  relowlpssretop  33183  1oequni2o  33187  curunc  33362  ptrest  33379  poimirlem16  33396  poimirlem30  33410  mblfinlem2  33418  ovoliunnfl  33422  voliunnfl  33424  itg2addnclem2  33433  ftc1anclem5  33460  ftc1anclem6  33461  sdc  33511  heiborlem3  33583  dvh4dimN  36555  dnnumch1  37433  aomclem6  37448  areaquad  37621  unitadd  38318  seff  38328  sblpnf  38329  hashnzfz  38339  lhe4.4ex1a  38348  iccdifioo  39544  itgsin0pilem1  39928  stoweidlem13  39993  stoweidlem26  40006  fourierdlem62  40148  fourierdlem102  40188  fourierdlem114  40200  fourierswlem  40210  fouriersw  40211  sge0tsms  40360  meaiuninc  40461  fmtno4prmfac  41249  41prothprm  41301  2zrngasgrp  41705  2zrngmsgrp  41712  mvlraddi  42279  mvlrmuli  42288  i2linesi  42289
  Copyright terms: Public domain W3C validator