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

Theorem eqtr3i 2455
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 2437 . 2  |-  B  =  A
3 eqtr3i.2 . 2  |-  A  =  C
42, 3eqtri 2453 1  |-  B  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-ex 1590  df-cleq 2426
This theorem is referenced by:  3eqtr3i  2461  3eqtr3ri  2462  unundi  3505  unundir  3506  inindi  3555  inindir  3556  dfin4  3578  difun1  3598  difabs  3602  notab  3608  dif0  3737  difdifdir  3754  tpidm13  3965  tpprceq3  4001  intmin2  4143  univ  4531  iunxpconst  4882  dmres  5119  opabresid  5147  rnresi  5170  cnvcnv  5278  rnresv  5285  cnvsn0  5295  cnvsn  5310  resdmres  5317  coi2  5342  coires1  5343  dfdm2  5357  isarep2  5486  resasplit  5569  ssimaex  5744  fnreseql  5801  fmptpr  5890  fnsuppeq0OLD  5926  resfunexg  5930  idref  5945  mpt2mpt  6171  caov31  6281  fvresex  6539  xpexgALT  6559  1st2val  6591  2nd2val  6592  fnsuppeq0  6706  ecopovtrn  7191  limensuci  7475  pssnn  7519  r1sucg  7964  jech9.3  8009  rankbnd2  8064  compss  8533  zorn2lem4  8656  iunfo  8691  cardf  8702  alephsuc3  8732  fpwwe2lem13  8796  rankcf  8931  halfnq  9132  addclprlem2  9173  mulgt0sr  9259  mul02lem2  9533  mul02  9534  addid1  9536  mvlladdi  9614  mvllmuli  10151  infmsup  10295  8th4div3  10532  nneo  10712  dec10  10772  nummac  10774  numadd  10776  numaddc  10777  nummul1c  10778  9p2e11  10804  decbin0  10845  rpsup  11688  resup  11689  om2uzrdg  11762  m1expcl2  11870  binom2aiOLD  11959  facnn  12036  fac0  12037  faclbnd4lem1  12052  hasheq0  12114  f1oun2prg  12510  sqr1  12744  sqr4  12745  sqr9  12746  rddif  12811  abs3lemi  12880  sumss2  13186  geo2sum2  13316  geomulcvg  13318  geoihalfsum  13324  sin0  13415  efival  13418  ef01bndlem  13450  cos2bnd  13454  sin4lt0  13461  2prm  13761  unbenlem  13951  dec5dvds  14075  modxai  14079  mod2xi  14080  mod2xnegi  14082  gcdi  14084  numexp2x  14090  decsplit  14094  setsid  14197  mreexexlem3d  14566  oppchom  14636  2oppchomf  14645  isoval  14685  oppchofcl  15052  oyoncl  15062  mvdco  15930  m1expaddsub  15983  psgn0fv0  15996  oppglsm  16120  dprd2da  16514  opprsubg  16661  lsppratlem1  17149  opsrtoslem1  17496  ply1basfvi  17593  coe1tm  17623  ply1coe  17642  zzngim  17826  cnmsgnsubg  17848  psgninv  17853  zrhpsgnmhm  17855  zrhpsgnodpm  17863  neitr  18625  kgeni  18951  xkoinjcn  19101  ufprim  19323  metreslem  19778  restmetu  20003  retopbas  20180  cnfldms  20196  qdensere2  20215  xrsmopn  20230  metdscn2  20274  pcoass  20437  iscmet3lem3  20642  cncms  20708  cnfldcusp  20710  resscdrg  20711  rrxprds  20734  ovoliunnul  20831  uniioombllem4  20907  vitalilem5  20933  mbfres  20963  ismbf3d  20973  i1fima  20997  i1fd  21000  itg2cnlem1  21080  itgss3  21133  ellimc2  21193  limccnp2  21208  cpnres  21252  lhop  21329  plyeq0  21563  plypf1  21564  sinhalfpilem  21809  sincos6thpi  21861  sincos3rdpi  21862  pige3  21863  dfrelog  21901  logimul  21947  logneg2  21948  dvlog  21980  cxpsqr  22032  ang180lem2  22090  ang180lem3  22091  ang180lem4  22092  quart1  22135  asin1  22173  atan0  22187  atanlogsublem  22194  atan1  22207  log2tlbnd  22224  log2ublem2  22226  log2ub  22228  basellem8  22309  cht2  22394  ppiub  22427  bposlem6  22512  bposlem8  22514  bposlem9  22515  lgsdir2lem3  22548  lgseisenlem1  22572  lgseisenlem2  22573  lgsquadlem1  22577  lgsquadlem2  22578  chebbnd1  22605  ax5seglem7  23003  ex-un  23453  circgrp  23683  ipdirilem  24051  ipasslem10  24061  hisubcomi  24328  normlem0  24333  norm3difi  24371  norm3lem  24373  polid2i  24381  chdmj1i  24706  chjjdiri  24749  spansn0  24766  pjoml4i  24812  cmbr3i  24825  qlaxr3i  24861  honpcani  25051  honpncani  25053  lnopunilem1  25236  lnophmlem2  25243  lnfn0i  25268  pjbdlni  25375  pjclem1  25421  pjclem3  25423  pjci  25426  atomli  25608  atabs2i  25628  mddmdin0i  25657  difeq  25722  disjdifprg  25742  imadifxp  25762  fnresin  25770  ofpreima2  25808  df1stres  25822  df2ndres  25823  cnvoprab  25846  ffsrn  25853  xrge0base  25968  xrge00  25969  xrge0mulgnn0  25972  xrge0slmod  26165  ordtconlem1  26207  xrge0iifcnv  26216  lmxrge0  26235  cnrrext  26292  esumpfinvallem  26376  measvuni  26481  measunl  26483  measinb  26488  mbfmcst  26527  sibfof  26573  eulerpartlemmf  26605  fib2  26632  fib3  26633  fib4  26634  fib5  26635  fib6  26636  0rrv  26681  coinfliprv  26712  ballotlem2  26718  ballotlemgun  26754  kur14lem6  26946  kur14lem7  26947  cvmlift2lem12  27050  problem5  27149  4bc3eq4  27236  divcnvshft  27244  divcnvlin  27245  risefall0lem  27375  bpoly2  28046  bpoly3  28047  ptrest  28266  mblfinlem2  28270  ovoliunnfl  28274  voliunnfl  28276  itg2addnclem2  28285  ftc1anclem5  28312  ftc1anclem6  28313  comppfsc  28420  sdc  28481  heiborlem3  28553  dnnumch1  29239  aomclem6  29254  areaquad  29434  seff  29437  sblpnf  29438  lhe4.4ex1a  29445  itgsin0pilem1  29633  stoweidlem13  29651  stoweidlem26  29664  mvlraddi  30823  mvlrmuli  30833  i2linesi  30834  bj-2upln1upl  32097  dvh4dimN  34662
  Copyright terms: Public domain W3C validator