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

Theorem eqtr3i 2498
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 2480 . 2  |-  B  =  A
3 eqtr3i.2 . 2  |-  A  =  C
42, 3eqtri 2496 1  |-  B  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  3eqtr3i  2504  3eqtr3ri  2505  unundi  3665  unundir  3666  inindi  3715  inindir  3716  dfin4  3738  difun1  3758  difabs  3762  notab  3768  dif0  3897  difdifdir  3914  tpidm13  4129  tpprceq3  4167  intmin2  4309  univ  4698  iunxpconst  5056  dmres  5294  opabresid  5327  rnresi  5350  cnvcnv  5459  rnresv  5466  cnvsn0  5476  cnvsn  5491  resdmres  5498  coi2  5524  coires1  5525  dfdm2  5539  isarep2  5668  resasplit  5755  ssimaex  5932  fnreseql  5991  fmptpr  6086  fnsuppeq0OLD  6122  resfunexg  6126  idref  6141  mpt2mpt  6378  caov31  6488  fvresex  6757  xpexgALT  6777  1st2val  6810  2nd2val  6811  fnsuppeq0  6928  ecopovtrn  7414  limensuci  7693  pssnn  7738  r1sucg  8187  jech9.3  8232  rankbnd2  8287  compss  8756  zorn2lem4  8879  iunfo  8914  cardf  8925  alephsuc3  8955  fpwwe2lem13  9020  rankcf  9155  halfnq  9354  addclprlem2  9395  mulgt0sr  9482  mul02lem2  9756  mul02  9757  addid1  9759  mvlladdi  9837  mvllmuli  10377  infmsup  10521  8th4div3  10759  nneo  10944  dec10  11006  nummac  11008  numadd  11010  numaddc  11011  nummul1c  11012  9p2e11  11038  decbin0  11079  rpsup  11961  resup  11962  om2uzrdg  12035  m1expcl2  12156  binom2aiOLD  12246  facnn  12323  fac0  12324  faclbnd4lem1  12339  hasheq0  12401  f1oun2prg  12828  sqrt1  13068  sqrt4  13069  sqrt9  13070  rddif  13136  abs3lemi  13205  sumss2  13511  geo2sum2  13646  geomulcvg  13648  geoihalfsum  13654  sin0  13745  efival  13748  ef01bndlem  13780  cos2bnd  13784  sin4lt0  13791  2prm  14092  unbenlem  14285  dec5dvds  14409  modxai  14413  mod2xi  14414  mod2xnegi  14416  gcdi  14418  numexp2x  14424  decsplit  14428  setsid  14531  mreexexlem3d  14901  oppchom  14971  2oppchomf  14980  isoval  15020  oppchofcl  15387  oyoncl  15397  mvdco  16276  m1expaddsub  16329  psgn0fv0  16342  oppglsm  16468  dprd2da  16893  opprsubg  17086  lsppratlem1  17593  opsrtoslem1  17947  ply1basfvi  18081  coe1tm  18113  ply1coe  18136  ply1coeOLD  18137  zzngim  18386  cnmsgnsubg  18408  psgninv  18413  zrhpsgnmhm  18415  zrhpsgnodpm  18423  neitr  19475  kgeni  19801  xkoinjcn  19951  ufprim  20173  metreslem  20628  restmetu  20853  retopbas  21030  cnfldms  21046  qdensere2  21065  xrsmopn  21080  metdscn2  21124  pcoass  21287  iscmet3lem3  21492  cncms  21558  cnfldcusp  21560  resscdrg  21561  rrxprds  21584  ovoliunnul  21681  uniioombllem4  21758  vitalilem5  21784  mbfres  21814  ismbf3d  21824  i1fima  21848  i1fd  21851  itg2cnlem1  21931  itgss3  21984  ellimc2  22044  limccnp2  22059  cpnres  22103  lhop  22180  plyeq0  22371  plypf1  22372  sinhalfpilem  22617  sincos6thpi  22669  sincos3rdpi  22670  pige3  22671  dfrelog  22709  logimul  22755  logneg2  22756  dvlog  22788  cxpsqrt  22840  ang180lem2  22898  ang180lem3  22899  ang180lem4  22900  quart1  22943  asin1  22981  atan0  22995  atanlogsublem  23002  atan1  23015  log2tlbnd  23032  log2ublem2  23034  log2ub  23036  basellem8  23117  cht2  23202  ppiub  23235  bposlem6  23320  bposlem8  23322  bposlem9  23323  lgsdir2lem3  23356  lgseisenlem1  23380  lgseisenlem2  23381  lgsquadlem1  23385  lgsquadlem2  23386  chebbnd1  23413  motplusg  23685  ax5seglem7  23942  ex-un  24850  circgrp  25080  ipdirilem  25448  ipasslem10  25458  hisubcomi  25725  normlem0  25730  norm3difi  25768  norm3lem  25770  polid2i  25778  chdmj1i  26103  chjjdiri  26146  spansn0  26163  pjoml4i  26209  cmbr3i  26222  qlaxr3i  26258  honpcani  26448  honpncani  26450  lnopunilem1  26633  lnophmlem2  26640  lnfn0i  26665  pjbdlni  26772  pjclem1  26818  pjclem3  26820  pjci  26823  atomli  27005  atabs2i  27025  mddmdin0i  27054  difeq  27118  disjdifprg  27137  imadifxp  27159  fnresin  27171  ofpreima2  27208  df1stres  27222  df2ndres  27223  cnvoprab  27246  ffsrn  27252  xrge0base  27363  xrge00  27364  xrge0mulgnn0  27367  xrge0slmod  27525  ordtconlem1  27570  xrge0iifcnv  27579  lmxrge0  27598  cnrrext  27655  esumpfinvallem  27748  measvuni  27853  measunl  27855  measinb  27860  mbfmcst  27898  sibfof  27950  eulerpartlemmf  27982  fib2  28009  fib3  28010  fib4  28011  fib5  28012  fib6  28013  0rrv  28058  coinfliprv  28089  ballotlem2  28095  ballotlemgun  28131  kur14lem6  28323  kur14lem7  28324  cvmlift2lem12  28427  problem5  28526  4bc3eq4  28614  divcnvshft  28622  divcnvlin  28623  risefall0lem  28753  bpoly2  29424  bpoly3  29425  ptrest  29653  mblfinlem2  29657  ovoliunnfl  29661  voliunnfl  29663  itg2addnclem2  29672  ftc1anclem5  29699  ftc1anclem6  29700  comppfsc  29807  sdc  29868  heiborlem3  29940  dnnumch1  30622  aomclem6  30637  areaquad  30817  seff  30820  sblpnf  30821  hashnzfz  30853  lhe4.4ex1a  30862  itgsin0pilem1  31295  stoweidlem13  31341  stoweidlem26  31354  dirkertrigeqlem1  31426  mvlraddi  32279  mvlrmuli  32291  i2linesi  32292  bj-2upln1upl  33681  dvh4dimN  36262
  Copyright terms: Public domain W3C validator