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

Theorem eqtr3i 2435
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 2417 . 2  |-  B  =  A
3 eqtr3i.2 . 2  |-  A  =  C
42, 3eqtri 2433 1  |-  B  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-cleq 2396
This theorem is referenced by:  3eqtr3i  2441  3eqtr3ri  2442  unundi  3606  unundir  3607  inindi  3658  inindir  3659  dfin4  3692  difun1  3712  difabs  3716  notab  3722  dif0  3844  difdifdir  3861  tpidm13  4076  tpprceq3  4114  intmin2  4257  univ  4644  iunxpconst  4882  dmres  5116  opabresid  5149  rnresi  5172  cnvcnv  5278  rnresv  5285  cnvsn0  5294  cnvsn  5309  resdmres  5316  coi2  5342  coires1  5343  dfdm2  5358  isarep2  5651  resasplit  5740  ssimaex  5916  fnreseql  5977  resfunexg  6120  idref  6136  mpt2mpt  6377  caov31  6487  fvresex  6759  xpexgALT  6779  1st2val  6812  2nd2val  6813  fnsuppeq0  6933  ecopovtrn  7453  limensuci  7733  pssnn  7775  r1sucg  8221  jech9.3  8266  rankbnd2  8321  compss  8790  zorn2lem4  8913  iunfo  8948  cardf  8959  alephsuc3  8989  fpwwe2lem13  9052  rankcf  9187  halfnq  9386  addclprlem2  9427  mulgt0sr  9514  mul02lem2  9793  mul02  9794  addid1  9796  mvlladdi  9875  mvllmuli  10420  infmsup  10563  8th4div3  10802  nneo  10989  dec10  11051  nummac  11053  numadd  11055  numaddc  11056  nummul1c  11057  9p2e11  11083  decbin0  11124  rpsup  12033  resup  12034  om2uzrdg  12110  m1expcl2  12234  facnn  12401  fac0  12402  faclbnd4lem1  12417  4bc3eq4  12452  hasheq0  12483  f1oun2prg  12923  sqrt1  13256  sqrt4  13257  sqrt9  13258  rddif  13324  abs3lemi  13393  sumss2  13699  divcnvshft  13820  geo2sum2  13837  geomulcvg  13839  geoihalfsum  13845  risefall0lem  13973  bpoly2  14004  bpoly3  14005  sin0  14095  efival  14098  ef01bndlem  14130  cos2bnd  14134  sin4lt0  14141  2prm  14444  unbenlem  14637  dec5dvds  14761  modxai  14765  mod2xi  14766  mod2xnegi  14768  gcdi  14770  numexp2x  14776  decsplit  14780  setsid  14886  mreexexlem3d  15262  oppchom  15330  2oppchomf  15339  isoval  15380  estrres  15734  oppchofcl  15855  oyoncl  15865  mvdco  16796  m1expaddsub  16849  psgn0fv0  16862  oppglsm  16988  dprd2da  17413  ring1  17570  opprsubg  17607  lsppratlem1  18115  opsrtoslem1  18470  ply1basfvi  18604  coe1tm  18636  ply1coe  18659  ply1coeOLD  18660  zzngim  18891  cnmsgnsubg  18913  psgninv  18918  zrhpsgnmhm  18920  neitr  19976  comppfsc  20327  kgeni  20332  xkoinjcn  20482  ufprim  20704  metreslem  21159  restmetu  21384  retopbas  21561  cnfldms  21577  qdensere2  21596  xrsmopn  21611  metdscn2  21655  pcoass  21818  iscmet3lem3  22023  cncms  22089  cnfldcusp  22091  resscdrg  22092  rrxprds  22115  ovoliunnul  22212  uniioombllem4  22289  vitalilem5  22315  mbfres  22345  ismbf3d  22355  i1fima  22379  i1fd  22382  itg2cnlem1  22462  itgss3  22515  ellimc2  22575  limccnp2  22590  cpnres  22634  lhop  22711  plyeq0  22902  plypf1  22903  sinhalfpilem  23150  sincos6thpi  23202  sincos3rdpi  23203  pige3  23204  dfrelog  23247  logimul  23295  logneg2  23296  dvlog  23328  cxpsqrt  23380  ang180lem2  23471  ang180lem3  23472  ang180lem4  23473  quart1  23514  asin1  23552  atan0  23566  atanlogsublem  23573  atan1  23586  log2tlbnd  23603  log2ublem2  23605  log2ub  23607  basellem8  23744  cht2  23829  ppiub  23862  bposlem6  23947  bposlem8  23949  bposlem9  23950  lgsdir2lem3  23983  lgseisenlem1  24007  lgseisenlem2  24008  lgsquadlem1  24012  lgsquadlem2  24013  chebbnd1  24040  istrkg3ld  24239  motplusg  24314  ax5seglem7  24667  ex-un  25575  circgrpOLD  25803  ipdirilem  26171  ipasslem10  26181  hisubcomi  26448  normlem0  26453  norm3difi  26491  norm3lem  26493  polid2i  26501  chdmj1i  26826  chjjdiri  26869  spansn0  26886  pjoml4i  26932  cmbr3i  26945  qlaxr3i  26981  honpcani  27170  honpncani  27172  lnopunilem1  27355  lnophmlem2  27362  lnfn0i  27387  pjbdlni  27494  pjclem1  27540  pjclem3  27542  pjci  27545  atomli  27727  atabs2i  27747  mddmdin0i  27776  difeq  27843  iunxdif3  27870  disjdifprg  27880  imadifxp  27907  fnresin  27924  ofpreima2  27964  df1stres  27979  df2ndres  27980  cnvoprab  28006  xrge0base  28138  xrge00  28139  xrge0mulgnn0  28142  xrge0slmod  28300  ordtconlem1  28372  xrge0iifcnv  28381  lmxrge0  28400  cnrrext  28456  esumrnmpt2  28528  esumpfinvallem  28534  unelldsys  28619  ldgenpisyslem1  28624  measvuni  28675  measunl  28677  measinb  28682  mbfmcst  28720  difelcarsg  28771  carsggect  28779  sibfof  28801  eulerpartlemmf  28833  fib2  28860  fib3  28861  fib4  28862  fib5  28863  fib6  28864  0rrv  28909  coinfliprv  28940  ballotlem2  28946  ballotlemgun  28982  kur14lem6  29521  kur14lem7  29522  cvmlift2lem12  29624  problem5  29888  quad3  29889  divcnvlin  29953  logi  29956  bj-2upln1upl  31160  relowlssretop  31293  relowlpssretop  31294  ptrest  31433  mblfinlem2  31437  ovoliunnfl  31441  voliunnfl  31443  itg2addnclem2  31453  ftc1anclem5  31480  ftc1anclem6  31481  sdc  31532  heiborlem3  31604  dvh4dimN  34480  dnnumch1  35365  aomclem6  35380  areaquad  35561  unitadd  36040  seff  36050  sblpnf  36051  hashnzfz  36086  lhe4.4ex1a  36095  iccdifioo  36936  itgsin0pilem1  37129  stoweidlem13  37176  stoweidlem26  37189  fourierdlem62  37332  fourierdlem102  37372  fourierdlem114  37384  fourierswlem  37394  fouriersw  37395  41prothprm  37878  2zrngasgrp  38270  2zrngmsgrp  38277  mvlraddi  38837  mvlrmuli  38849  i2linesi  38850
  Copyright terms: Public domain W3C validator