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

Theorem eqtr3i 2426
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 2408 . 2  |-  B  =  A
3 eqtr3i.2 . 2  |-  A  =  C
42, 3eqtri 2424 1  |-  B  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1649
This theorem is referenced by:  3eqtr3i  2432  3eqtr3ri  2433  unundi  3468  unundir  3469  inindi  3518  inindir  3519  dfin4  3541  difun1  3561  difabs  3565  notab  3571  dfrab2  3576  dif0  3658  difdifdir  3675  tpidm13  3866  tpprceq3  3898  intmin2  4037  univ  4713  iunxpconst  4893  dmres  5126  opabresid  5153  rnresi  5178  cnvcnv  5282  rnresv  5289  cnvsn0  5297  cnvsn  5311  resdmres  5320  coi2  5345  coires1  5346  dfdm2  5360  isarep2  5492  resasplit  5572  ssimaex  5747  fnreseql  5799  fnsuppeq0  5912  resfunexg  5916  idref  5938  fvresex  5941  mpt2mpt  6124  caov31  6235  xpexgALT  6256  1st2val  6331  2nd2val  6332  ecopovtrn  6966  limensuci  7242  pssnn  7286  r1sucg  7651  jech9.3  7696  rankbnd2  7751  compss  8212  zorn2lem4  8335  iunfo  8370  cardf  8381  alephsuc3  8411  fpwwe2lem13  8473  rankcf  8608  halfnq  8809  addclprlem2  8850  mulgt0sr  8936  mul02lem2  9199  mul02  9200  addid1  9202  infmsup  9942  8th4div3  10147  nneo  10309  dec10  10368  nummac  10370  numadd  10372  numaddc  10373  nummul1c  10374  9p2e11  10400  decbin0  10441  rpsup  11202  resup  11203  om2uzrdg  11251  m1expcl2  11358  binom2aiOLD  11446  facnn  11523  fac0  11524  faclbnd4lem1  11539  hasheq0  11599  f1oun2prg  11819  sqr1  12032  sqr4  12033  sqr9  12034  rddif  12099  abs3lemi  12168  sumss2  12475  geo2sum2  12606  geomulcvg  12608  geoihalfsum  12614  sin0  12705  efival  12708  ef01bndlem  12740  cos2bnd  12744  sin4lt0  12751  2prm  13050  unbenlem  13231  dec5dvds  13355  modxai  13359  mod2xi  13360  mod2xnegi  13362  gcdi  13364  numexp2x  13370  decsplit  13374  setsid  13463  mreexexlem3d  13826  oppchom  13896  2oppchomf  13905  isoval  13945  oppchofcl  14312  oyoncl  14322  oppglsm  15231  dprd2da  15555  opprsubg  15696  lsppratlem1  16174  opsrtoslem1  16499  ply1basfvi  16590  coe1tm  16620  ply1coe  16639  zzngim  16788  neitr  17198  kgeni  17522  xkoinjcn  17672  ufprim  17894  metreslem  18345  restmetu  18570  retopbas  18747  cnfldms  18763  qdensere2  18781  xrsmopn  18796  metdscn2  18840  pcoass  19002  iscmet3lem3  19196  cncms  19262  cnfldcusp  19264  resscdrg  19265  ovoliunnul  19356  uniioombllem4  19431  vitalilem5  19457  mbfres  19489  ismbf3d  19499  i1fima  19523  i1fd  19526  itg2cnlem1  19606  itgss3  19659  ellimc2  19717  limccnp2  19732  cpnres  19776  lhop  19853  plyeq0  20083  plypf1  20084  sinhalfpilem  20327  sincos6thpi  20376  sincos3rdpi  20377  pige3  20378  dfrelog  20416  logimul  20462  logneg2  20463  dvlog  20495  cxpsqr  20547  ang180lem2  20605  ang180lem3  20606  ang180lem4  20607  quart1  20649  asin1  20687  atan0  20701  atanlogsublem  20708  atan1  20721  log2tlbnd  20738  log2ublem2  20740  log2ub  20742  basellem8  20823  cht2  20908  ppiub  20941  bposlem6  21026  bposlem8  21028  bposlem9  21029  lgsdir2lem3  21062  lgseisenlem1  21086  lgseisenlem2  21087  lgsquadlem1  21091  lgsquadlem2  21092  chebbnd1  21119  ex-un  21685  circgrp  21915  ipdirilem  22283  ipasslem10  22293  hisubcomi  22559  normlem0  22564  norm3difi  22602  norm3lem  22604  polid2i  22612  chdmj1i  22936  chjjdiri  22979  spansn0  22996  pjoml4i  23042  cmbr3i  23055  qlaxr3i  23091  honpcani  23281  honpncani  23283  lnopunilem1  23466  lnophmlem2  23473  lnfn0i  23498  pjbdlni  23605  pjclem1  23651  pjclem3  23653  pjci  23656  atomli  23838  atabs2i  23858  mddmdin0i  23887  difeq  23951  disjdifprg  23970  imadifxp  23991  fmptpr  24015  df1stres  24044  df2ndres  24045  xrge0base  24160  xrge00  24161  xrge0mulgnn0  24163  xrge0iifcnv  24272  lmxrge0  24290  esumpfinvallem  24417  measvuni  24521  measunl  24523  measinb  24528  mbfmcst  24562  sibfof  24607  sitgclcn  24611  0rrv  24662  coinfliprv  24693  ballotlem2  24699  ballotlemgun  24735  kur14lem6  24850  kur14lem7  24851  cvmlift2lem12  24954  4bc3eq4  25156  divcnvshft  25164  divcnvlin  25165  risefall0lem  25294  ax5seglem7  25778  bpoly2  26007  bpoly3  26008  mblfinlem  26143  ovoliunnfl  26147  voliunnfl  26149  itg2addnclem2  26156  comppfsc  26277  sdc  26338  heiborlem3  26412  dnnumch1  27009  aomclem6  27024  mvdco  27256  m1expaddsub  27289  cnmsgnsubg  27302  seff  27406  sblpnf  27407  lhe4.4ex1a  27414  itgsin0pilem1  27611  stoweidlem13  27629  stoweidlem26  27642  dvh4dimN  31930
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator