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

Theorem eqtr3i 2465
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 2447 . 2  |-  B  =  A
3 eqtr3i.2 . 2  |-  A  =  C
42, 3eqtri 2463 1  |-  B  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436
This theorem is referenced by:  3eqtr3i  2471  3eqtr3ri  2472  unundi  3538  unundir  3539  inindi  3588  inindir  3589  dfin4  3611  difun1  3631  difabs  3635  notab  3641  dif0  3770  difdifdir  3787  tpidm13  3998  tpprceq3  4034  intmin2  4176  univ  4564  iunxpconst  4916  dmres  5152  opabresid  5180  rnresi  5203  cnvcnv  5311  rnresv  5318  cnvsn0  5328  cnvsn  5343  resdmres  5350  coi2  5375  coires1  5376  dfdm2  5390  isarep2  5519  resasplit  5602  ssimaex  5777  fnreseql  5834  fmptpr  5924  fnsuppeq0OLD  5960  resfunexg  5964  idref  5979  mpt2mpt  6203  caov31  6313  fvresex  6571  xpexgALT  6591  1st2val  6623  2nd2val  6624  fnsuppeq0  6738  ecopovtrn  7224  limensuci  7508  pssnn  7552  r1sucg  7997  jech9.3  8042  rankbnd2  8097  compss  8566  zorn2lem4  8689  iunfo  8724  cardf  8735  alephsuc3  8765  fpwwe2lem13  8830  rankcf  8965  halfnq  9166  addclprlem2  9207  mulgt0sr  9293  mul02lem2  9567  mul02  9568  addid1  9570  mvlladdi  9648  mvllmuli  10185  infmsup  10329  8th4div3  10566  nneo  10746  dec10  10806  nummac  10808  numadd  10810  numaddc  10811  nummul1c  10812  9p2e11  10838  decbin0  10879  rpsup  11726  resup  11727  om2uzrdg  11800  m1expcl2  11908  binom2aiOLD  11997  facnn  12074  fac0  12075  faclbnd4lem1  12090  hasheq0  12152  f1oun2prg  12548  sqr1  12782  sqr4  12783  sqr9  12784  rddif  12849  abs3lemi  12918  sumss2  13224  geo2sum2  13355  geomulcvg  13357  geoihalfsum  13363  sin0  13454  efival  13457  ef01bndlem  13489  cos2bnd  13493  sin4lt0  13500  2prm  13800  unbenlem  13990  dec5dvds  14114  modxai  14118  mod2xi  14119  mod2xnegi  14121  gcdi  14123  numexp2x  14129  decsplit  14133  setsid  14236  mreexexlem3d  14605  oppchom  14675  2oppchomf  14684  isoval  14724  oppchofcl  15091  oyoncl  15101  mvdco  15972  m1expaddsub  16025  psgn0fv0  16038  oppglsm  16162  dprd2da  16563  opprsubg  16750  lsppratlem1  17250  opsrtoslem1  17587  ply1basfvi  17718  coe1tm  17748  ply1coe  17768  ply1coeOLD  17769  zzngim  18007  cnmsgnsubg  18029  psgninv  18034  zrhpsgnmhm  18036  zrhpsgnodpm  18044  neitr  18806  kgeni  19132  xkoinjcn  19282  ufprim  19504  metreslem  19959  restmetu  20184  retopbas  20361  cnfldms  20377  qdensere2  20396  xrsmopn  20411  metdscn2  20455  pcoass  20618  iscmet3lem3  20823  cncms  20889  cnfldcusp  20891  resscdrg  20892  rrxprds  20915  ovoliunnul  21012  uniioombllem4  21088  vitalilem5  21114  mbfres  21144  ismbf3d  21154  i1fima  21178  i1fd  21181  itg2cnlem1  21261  itgss3  21314  ellimc2  21374  limccnp2  21389  cpnres  21433  lhop  21510  plyeq0  21701  plypf1  21702  sinhalfpilem  21947  sincos6thpi  21999  sincos3rdpi  22000  pige3  22001  dfrelog  22039  logimul  22085  logneg2  22086  dvlog  22118  cxpsqr  22170  ang180lem2  22228  ang180lem3  22229  ang180lem4  22230  quart1  22273  asin1  22311  atan0  22325  atanlogsublem  22332  atan1  22345  log2tlbnd  22362  log2ublem2  22364  log2ub  22366  basellem8  22447  cht2  22532  ppiub  22565  bposlem6  22650  bposlem8  22652  bposlem9  22653  lgsdir2lem3  22686  lgseisenlem1  22710  lgseisenlem2  22711  lgsquadlem1  22715  lgsquadlem2  22716  chebbnd1  22743  ax5seglem7  23203  ex-un  23653  circgrp  23883  ipdirilem  24251  ipasslem10  24261  hisubcomi  24528  normlem0  24533  norm3difi  24571  norm3lem  24573  polid2i  24581  chdmj1i  24906  chjjdiri  24949  spansn0  24966  pjoml4i  25012  cmbr3i  25025  qlaxr3i  25061  honpcani  25251  honpncani  25253  lnopunilem1  25436  lnophmlem2  25443  lnfn0i  25468  pjbdlni  25575  pjclem1  25621  pjclem3  25623  pjci  25626  atomli  25808  atabs2i  25828  mddmdin0i  25857  difeq  25921  disjdifprg  25941  imadifxp  25961  fnresin  25969  ofpreima2  26007  df1stres  26021  df2ndres  26022  cnvoprab  26045  ffsrn  26051  xrge0base  26168  xrge00  26169  xrge0mulgnn0  26172  xrge0slmod  26334  ordtconlem1  26376  xrge0iifcnv  26385  lmxrge0  26404  cnrrext  26461  esumpfinvallem  26545  measvuni  26650  measunl  26652  measinb  26657  mbfmcst  26696  sibfof  26748  eulerpartlemmf  26780  fib2  26807  fib3  26808  fib4  26809  fib5  26810  fib6  26811  0rrv  26856  coinfliprv  26887  ballotlem2  26893  ballotlemgun  26929  kur14lem6  27121  kur14lem7  27122  cvmlift2lem12  27225  problem5  27324  4bc3eq4  27412  divcnvshft  27420  divcnvlin  27421  risefall0lem  27551  bpoly2  28222  bpoly3  28223  ptrest  28451  mblfinlem2  28455  ovoliunnfl  28459  voliunnfl  28461  itg2addnclem2  28470  ftc1anclem5  28497  ftc1anclem6  28498  comppfsc  28605  sdc  28666  heiborlem3  28738  dnnumch1  29423  aomclem6  29438  areaquad  29618  seff  29621  sblpnf  29622  lhe4.4ex1a  29629  itgsin0pilem1  29816  stoweidlem13  29834  stoweidlem26  29847  mvlraddi  31213  mvlrmuli  31225  i2linesi  31226  bj-2upln1upl  32613  dvh4dimN  35188
  Copyright terms: Public domain W3C validator