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

Theorem eqtr3i 2318
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 2300 . 2  |-  B  =  A
3 eqtr3i.2 . 2  |-  A  =  C
42, 3eqtri 2316 1  |-  B  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1632
This theorem is referenced by:  3eqtr3i  2324  3eqtr3ri  2325  unundi  3349  unundir  3350  inindi  3399  inindir  3400  dfin4  3422  difun1  3441  difabs  3445  notab  3451  dfrab2  3456  dif0  3537  difdifdir  3554  tpidm13  3742  intmin2  3905  univ  4581  iunxpconst  4762  dmres  4992  opabresid  5019  rnresi  5044  cnvcnv  5142  rnresv  5149  cnvsn0  5157  cnvsn  5171  resdmres  5180  coi2  5205  coires1  5206  dfdm2  5220  isarep2  5348  resasplit  5427  ssimaex  5600  fnreseql  5651  fnsuppeq0  5749  resfunexg  5753  idref  5775  fvresex  5778  mpt2mpt  5955  caov31  6065  xpexgALT  6086  1st2val  6161  2nd2val  6162  ecopovtrn  6777  limensuci  7053  pssnn  7097  r1sucg  7457  jech9.3  7502  rankbnd2  7557  compss  8018  zorn2lem4  8142  iunfo  8177  cardf  8188  alephsuc3  8218  fpwwe2lem13  8280  rankcf  8415  halfnq  8616  addclprlem2  8657  mulgt0sr  8743  mul02lem2  9005  mul02  9006  addid1  9008  infmsup  9748  8th4div3  9951  nneo  10111  dec10  10170  nummac  10172  numadd  10174  numaddc  10175  nummul1c  10176  9p2e11  10202  decbin0  10243  rpsup  10986  resup  10987  om2uzrdg  11035  m1expcl2  11141  binom2aiOLD  11229  facnn  11306  fac0  11307  faclbnd4lem1  11322  hasheq0  11369  sqr1  11773  sqr4  11774  sqr9  11775  rddif  11840  abs3lemi  11909  sumss2  12215  geo2sum2  12346  geomulcvg  12348  geoihalfsum  12354  sin0  12445  efival  12448  ef01bndlem  12480  cos2bnd  12484  sin4lt0  12491  2prm  12790  unbenlem  12971  dec5dvds  13095  modxai  13099  mod2xi  13100  mod2xnegi  13102  gcdi  13104  numexp2x  13110  decsplit  13114  setsid  13203  mreexexlem3d  13564  oppchom  13634  2oppchomf  13643  isoval  13683  oppchofcl  14050  oyoncl  14060  oppglsm  14969  dprd2da  15293  opprsubg  15434  lsppratlem1  15916  opsrtoslem1  16241  ply1basfvi  16335  coe1tm  16365  ply1coe  16384  zzngim  16522  kgeni  17248  xkoinjcn  17397  ufprim  17620  metreslem  17942  retopbas  18285  cnfldms  18301  qdensere2  18319  xrsmopn  18334  metdscn2  18377  pcoass  18538  iscmet3lem3  18732  cncms  18790  resscdrg  18791  ovoliunnul  18882  uniioombllem4  18957  vitalilem5  18983  mbfres  19015  ismbf3d  19025  i1fima  19049  i1fd  19052  itg2cnlem1  19132  itgss3  19185  ellimc2  19243  limccnp2  19258  cpnres  19302  lhop  19379  plyeq0  19609  plypf1  19610  sinhalfpilem  19850  sincos6thpi  19899  sincos3rdpi  19900  pige3  19901  dfrelog  19939  logimul  19984  logneg2  19985  dvlog  20014  cxpsqr  20066  ang180lem2  20124  ang180lem3  20125  ang180lem4  20126  quart1  20168  asin1  20206  atan0  20220  atanlogsublem  20227  atan1  20240  log2tlbnd  20257  log2ublem2  20259  log2ub  20261  basellem8  20341  cht2  20426  ppiub  20459  bposlem6  20544  bposlem8  20546  bposlem9  20547  lgsdir2lem3  20580  lgseisenlem1  20604  lgseisenlem2  20605  lgsquadlem1  20609  lgsquadlem2  20610  chebbnd1  20637  ex-un  20827  circgrp  21057  ipdirilem  21423  ipasslem10  21433  hisubcomi  21699  normlem0  21704  norm3difi  21742  norm3lem  21744  polid2i  21752  chdmj1i  22076  chjjdiri  22119  spansn0  22136  pjoml4i  22182  cmbr3i  22195  qlaxr3i  22231  honpcani  22421  honpncani  22423  lnopunilem1  22606  lnophmlem2  22613  lnfn0i  22638  pjbdlni  22745  pjclem1  22791  pjclem3  22793  pjci  22796  atomli  22978  atabs2i  22998  mddmdin0i  23027  ballotlem1  23061  ballotlem2  23063  ballotlemfval0  23070  ballotlemgun  23099  ballotth  23112  difeq  23144  xppreima  23226  fmptpr  23229  partfun  23255  df1stres  23258  df2ndres  23259  xrge0base  23325  xrge00  23326  xrge0mulgnn0  23328  disjdifprg  23367  lmxrge0  23390  esumpfinvallem  23457  measinb  23563  mbfmcst  23579  0rrv  23669  coinfliprv  23698  kur14lem6  23757  kur14lem7  23758  cvmlift2lem12  23860  4bc3eq4  24113  ax5seglem7  24635  bpoly2  24864  bpoly3  24865  ovoliunnfl  25001  itg2addnclem2  25004  toplat  25393  selsubf3  26094  comppfsc  26410  sdc  26557  heiborlem3  26640  dnnumch1  27244  aomclem6  27259  mvdco  27491  m1expaddsub  27524  cnmsgnsubg  27537  seff  27641  sblpnf  27642  lhe4.4ex1a  27649  dvcosre  27844  itgsin0pilem1  27847  stoweidlem13  27865  stoweidlem26  27878  stoweidlem34  27886  tpprceq3  28182  f1oun2prg  28187  dvh4dimN  32259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator