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

Theorem eqtr3i 2458
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 2440 . 2  |-  B  =  A
3 eqtr3i.2 . 2  |-  A  =  C
42, 3eqtri 2456 1  |-  B  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1652
This theorem is referenced by:  3eqtr3i  2464  3eqtr3ri  2465  unundi  3508  unundir  3509  inindi  3558  inindir  3559  dfin4  3581  difun1  3601  difabs  3605  notab  3611  dfrab2  3616  dif0  3698  difdifdir  3715  tpidm13  3906  tpprceq3  3938  intmin2  4077  univ  4754  iunxpconst  4934  dmres  5167  opabresid  5194  rnresi  5219  cnvcnv  5323  rnresv  5330  cnvsn0  5338  cnvsn  5352  resdmres  5361  coi2  5386  coires1  5387  dfdm2  5401  isarep2  5533  resasplit  5613  ssimaex  5788  fnreseql  5840  fnsuppeq0  5953  resfunexg  5957  idref  5979  fvresex  5982  mpt2mpt  6165  caov31  6276  xpexgALT  6297  1st2val  6372  2nd2val  6373  ecopovtrn  7007  limensuci  7283  pssnn  7327  r1sucg  7695  jech9.3  7740  rankbnd2  7795  compss  8256  zorn2lem4  8379  iunfo  8414  cardf  8425  alephsuc3  8455  fpwwe2lem13  8517  rankcf  8652  halfnq  8853  addclprlem2  8894  mulgt0sr  8980  mul02lem2  9243  mul02  9244  addid1  9246  infmsup  9986  8th4div3  10191  nneo  10353  dec10  10412  nummac  10414  numadd  10416  numaddc  10417  nummul1c  10418  9p2e11  10444  decbin0  10485  rpsup  11247  resup  11248  om2uzrdg  11296  m1expcl2  11403  binom2aiOLD  11491  facnn  11568  fac0  11569  faclbnd4lem1  11584  hasheq0  11644  f1oun2prg  11864  sqr1  12077  sqr4  12078  sqr9  12079  rddif  12144  abs3lemi  12213  sumss2  12520  geo2sum2  12651  geomulcvg  12653  geoihalfsum  12659  sin0  12750  efival  12753  ef01bndlem  12785  cos2bnd  12789  sin4lt0  12796  2prm  13095  unbenlem  13276  dec5dvds  13400  modxai  13404  mod2xi  13405  mod2xnegi  13407  gcdi  13409  numexp2x  13415  decsplit  13419  setsid  13508  mreexexlem3d  13871  oppchom  13941  2oppchomf  13950  isoval  13990  oppchofcl  14357  oyoncl  14367  oppglsm  15276  dprd2da  15600  opprsubg  15741  lsppratlem1  16219  opsrtoslem1  16544  ply1basfvi  16635  coe1tm  16665  ply1coe  16684  zzngim  16833  neitr  17244  kgeni  17569  xkoinjcn  17719  ufprim  17941  metreslem  18392  restmetu  18617  retopbas  18794  cnfldms  18810  qdensere2  18828  xrsmopn  18843  metdscn2  18887  pcoass  19049  iscmet3lem3  19243  cncms  19309  cnfldcusp  19311  resscdrg  19312  ovoliunnul  19403  uniioombllem4  19478  vitalilem5  19504  mbfres  19536  ismbf3d  19546  i1fima  19570  i1fd  19573  itg2cnlem1  19653  itgss3  19706  ellimc2  19764  limccnp2  19779  cpnres  19823  lhop  19900  plyeq0  20130  plypf1  20131  sinhalfpilem  20374  sincos6thpi  20423  sincos3rdpi  20424  pige3  20425  dfrelog  20463  logimul  20509  logneg2  20510  dvlog  20542  cxpsqr  20594  ang180lem2  20652  ang180lem3  20653  ang180lem4  20654  quart1  20696  asin1  20734  atan0  20748  atanlogsublem  20755  atan1  20768  log2tlbnd  20785  log2ublem2  20787  log2ub  20789  basellem8  20870  cht2  20955  ppiub  20988  bposlem6  21073  bposlem8  21075  bposlem9  21076  lgsdir2lem3  21109  lgseisenlem1  21133  lgseisenlem2  21134  lgsquadlem1  21138  lgsquadlem2  21139  chebbnd1  21166  ex-un  21732  circgrp  21962  ipdirilem  22330  ipasslem10  22340  hisubcomi  22606  normlem0  22611  norm3difi  22649  norm3lem  22651  polid2i  22659  chdmj1i  22983  chjjdiri  23026  spansn0  23043  pjoml4i  23089  cmbr3i  23102  qlaxr3i  23138  honpcani  23328  honpncani  23330  lnopunilem1  23513  lnophmlem2  23520  lnfn0i  23545  pjbdlni  23652  pjclem1  23698  pjclem3  23700  pjci  23703  atomli  23885  atabs2i  23905  mddmdin0i  23934  difeq  23998  disjdifprg  24017  imadifxp  24038  fmptpr  24062  df1stres  24091  df2ndres  24092  xrge0base  24207  xrge00  24208  xrge0mulgnn0  24210  xrge0iifcnv  24319  lmxrge0  24337  esumpfinvallem  24464  measvuni  24568  measunl  24570  measinb  24575  mbfmcst  24609  sibfof  24654  sitgclcn  24658  0rrv  24709  coinfliprv  24740  ballotlem2  24746  ballotlemgun  24782  kur14lem6  24897  kur14lem7  24898  cvmlift2lem12  25001  4bc3eq4  25203  divcnvshft  25211  divcnvlin  25212  risefall0lem  25342  ax5seglem7  25874  bpoly2  26103  bpoly3  26104  mblfinlem2  26244  ovoliunnfl  26248  voliunnfl  26250  itg2addnclem2  26257  ftc1anclem5  26284  ftc1anclem6  26285  comppfsc  26387  sdc  26448  heiborlem3  26522  dnnumch1  27119  aomclem6  27134  mvdco  27365  m1expaddsub  27398  cnmsgnsubg  27411  seff  27515  sblpnf  27516  lhe4.4ex1a  27523  itgsin0pilem1  27720  stoweidlem13  27738  stoweidlem26  27751  dvh4dimN  32245
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator