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

Theorem eqtr3i 2305
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 2287 . 2  |-  B  =  A
3 eqtr3i.2 . 2  |-  A  =  C
42, 3eqtri 2303 1  |-  B  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1623
This theorem is referenced by:  3eqtr3i  2311  3eqtr3ri  2312  unundi  3336  unundir  3337  inindi  3386  inindir  3387  dfin4  3409  difun1  3428  difabs  3432  notab  3438  dfrab2  3443  dif0  3524  difdifdir  3541  tpidm13  3729  intmin2  3889  univ  4565  iunxpconst  4746  dmres  4976  opabresid  5003  rnresi  5028  cnvcnv  5126  rnresv  5133  cnvsn0  5141  cnvsn  5155  resdmres  5164  coi2  5189  coires1  5190  dfdm2  5204  isarep2  5332  resasplit  5411  ssimaex  5584  fnreseql  5635  fnsuppeq0  5733  resfunexg  5737  idref  5759  fvresex  5762  mpt2mpt  5939  caov31  6049  xpexgALT  6070  1st2val  6145  2nd2val  6146  ecopovtrn  6761  limensuci  7037  pssnn  7081  r1sucg  7441  jech9.3  7486  rankbnd2  7541  compss  8002  zorn2lem4  8126  iunfo  8161  cardf  8172  alephsuc3  8202  fpwwe2lem13  8264  rankcf  8399  halfnq  8600  addclprlem2  8641  mulgt0sr  8727  mul02lem2  8989  mul02  8990  addid1  8992  infmsup  9732  8th4div3  9935  nneo  10095  dec10  10154  nummac  10156  numadd  10158  numaddc  10159  nummul1c  10160  9p2e11  10186  decbin0  10227  rpsup  10970  resup  10971  om2uzrdg  11019  m1expcl2  11125  binom2aiOLD  11213  facnn  11290  fac0  11291  faclbnd4lem1  11306  hasheq0  11353  sqr1  11757  sqr4  11758  sqr9  11759  rddif  11824  abs3lemi  11893  sumss2  12199  geo2sum2  12330  geomulcvg  12332  geoihalfsum  12338  sin0  12429  efival  12432  ef01bndlem  12464  cos2bnd  12468  sin4lt0  12475  2prm  12774  unbenlem  12955  dec5dvds  13079  modxai  13083  mod2xi  13084  mod2xnegi  13086  gcdi  13088  numexp2x  13094  decsplit  13098  setsid  13187  mreexexlem3d  13548  oppchom  13618  2oppchomf  13627  isoval  13667  oppchofcl  14034  oyoncl  14044  oppglsm  14953  dprd2da  15277  opprsubg  15418  lsppratlem1  15900  opsrtoslem1  16225  ply1basfvi  16319  coe1tm  16349  ply1coe  16368  zzngim  16506  kgeni  17232  xkoinjcn  17381  ufprim  17604  metreslem  17926  retopbas  18269  cnfldms  18285  qdensere2  18303  xrsmopn  18318  metdscn2  18361  pcoass  18522  iscmet3lem3  18716  cncms  18774  resscdrg  18775  ovoliunnul  18866  uniioombllem4  18941  vitalilem5  18967  mbfres  18999  ismbf3d  19009  i1fima  19033  i1fd  19036  itg2cnlem1  19116  itgss3  19169  ellimc2  19227  limccnp2  19242  cpnres  19286  lhop  19363  plyeq0  19593  plypf1  19594  sinhalfpilem  19834  sincos6thpi  19883  sincos3rdpi  19884  pige3  19885  dfrelog  19923  logimul  19968  logneg2  19969  dvlog  19998  cxpsqr  20050  ang180lem2  20108  ang180lem3  20109  ang180lem4  20110  quart1  20152  asin1  20190  atan0  20204  atanlogsublem  20211  atan1  20224  log2tlbnd  20241  log2ublem2  20243  log2ub  20245  basellem8  20325  cht2  20410  ppiub  20443  bposlem6  20528  bposlem8  20530  bposlem9  20531  lgsdir2lem3  20564  lgseisenlem1  20588  lgseisenlem2  20589  lgsquadlem1  20593  lgsquadlem2  20594  chebbnd1  20621  ex-un  20811  circgrp  21041  ipdirilem  21407  ipasslem10  21417  hisubcomi  21683  normlem0  21688  norm3difi  21726  norm3lem  21728  polid2i  21736  chdmj1i  22060  chjjdiri  22103  spansn0  22120  pjoml4i  22166  cmbr3i  22179  qlaxr3i  22215  honpcani  22405  honpncani  22407  lnopunilem1  22590  lnophmlem2  22597  lnfn0i  22622  pjbdlni  22729  pjclem1  22775  pjclem3  22777  pjci  22780  atomli  22962  atabs2i  22982  mddmdin0i  23011  ballotlem1  23045  ballotlem2  23047  ballotlemfval0  23054  ballotlemgun  23083  ballotth  23096  kur14lem6  23153  kur14lem7  23154  cvmlift2lem12  23256  4bc3eq4  23509  ax5seglem7  23974  bpoly2  24203  bpoly3  24204  repfuntw  24572  toplat  24702  selsubf3  25403  comppfsc  25719  sdc  25866  heiborlem3  25949  dnnumch1  26553  aomclem6  26568  mvdco  26800  m1expaddsub  26833  cnmsgnsubg  26846  seff  26950  sblpnf  26951  lhe4.4ex1a  26958  dvcosre  27153  itgsin0pilem1  27156  stoweidlem13  27174  stoweidlem26  27187  stoweidlem34  27195  tpprceq3  27483  f1oun2prg  27487  dvh4dimN  31010
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator