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

Theorem eqtr3i 2785
Description: An equality transitivity inference. (Contributed by NM, 6-May-1994.)
Hypotheses
Ref Expression
eqtr3i.1 𝐴 = 𝐵
eqtr3i.2 𝐴 = 𝐶
Assertion
Ref Expression
eqtr3i 𝐵 = 𝐶

Proof of Theorem eqtr3i
StepHypRef Expression
1 eqtr3i.1 . . 3 𝐴 = 𝐵
21eqcomi 2770 . 2 𝐵 = 𝐴
3 eqtr3i.2 . 2 𝐴 = 𝐶
42, 3eqtri 2783 1 𝐵 = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2754
This theorem is referenced by:  3eqtr3i  2791  3eqtr3ri  2792  unundi  3918  unundir  3919  inindi  3974  inindir  3975  dfin4  4011  difun1  4031  difabs  4036  notab  4041  dif0  4094  difdifdir  4201  tpidm13  4436  intmin2  4657  iunxdif3  4759  univ  5069  iunxpconst  5333  dmres  5578  opabresid  5614  rnresi  5638  cnvcnvOLD  5746  rnresv  5753  cnvsn0  5762  cnvsnOLD  5780  resdmres  5787  coi2  5814  coires1  5815  dfdm2  5829  isarep2  6140  resasplit  6236  ssimaex  6427  fnreseql  6492  resfunexg  6645  idref  6664  mpt2mpt  6919  caov31  7030  fvresex  7306  xpexgALT  7328  1st2val  7363  2nd2val  7364  cnvoprab  7399  fnsuppeq0  7494  ecopovtrn  8020  limensuci  8304  pssnn  8346  r1sucg  8808  jech9.3  8853  rankbnd2  8908  djuin  8956  compss  9411  zorn2lem4  9534  iunfo  9574  cardf  9585  alephsuc3  9615  fpwwe2lem13  9677  rankcf  9812  halfnq  10011  addclprlem2  10052  mulgt0sr  10139  mul02lem2  10426  mul02  10427  addid1  10429  mvlladdi  10512  mvllmuli  11071  infrenegsup  11219  8th4div3  11465  nneo  11674  dec10OLD  11768  nummac  11771  numadd  11773  numaddc  11774  nummul1c  11775  9p2e11OLD  11833  decbin0  11895  rpsup  12880  resup  12881  om2uzrdg  12970  m1expcl2  13097  facnn  13277  fac0  13278  faclbnd4lem1  13295  4bc3eq4  13330  hasheq0  13367  f1oun2prg  13883  sqrt1  14232  sqrt4  14233  sqrt9  14234  rddif  14300  abs3lemi  14369  sumss2  14677  divcnvshft  14807  geo2sum2  14825  geomulcvg  14827  geoihalfsum  14834  risefall0lem  14977  bpoly2  15008  bpoly3  15009  sin0  15099  efival  15102  ef01bndlem  15134  cos2bnd  15138  sin4lt0  15145  flodddiv4  15360  2prm  15628  unbenlem  15835  dec5dvds  15991  modxai  15995  mod2xi  15996  mod2xnegi  15998  gcdi  16000  numexp2x  16006  decsplit  16010  decsplitOLD  16014  setsid  16137  mreexexlem3d  16529  oppchom  16597  2oppchomf  16606  isoval  16647  estrres  17001  oppchofcl  17122  oyoncl  17132  mvdco  18086  m1expaddsub  18139  psgn0fv0  18152  oppglsm  18278  dprd2da  18662  ring1  18823  opprsubg  18857  lsppratlem1  19370  opsrtoslem1  19707  ply1basfvi  19834  coe1tm  19866  ply1coe  19889  zzngim  20124  cnmsgnsubg  20146  psgninv  20151  zrhpsgnmhm  20153  neitr  21207  comppfsc  21558  kgeni  21563  xkoinjcn  21713  ufprim  21935  metreslem  22389  restmetu  22597  retopbas  22786  cnfldms  22801  qdensere2  22822  xrsmopn  22837  metdscn2  22882  pcoass  23045  recvs  23167  zclmncvs  23169  iscmet3lem3  23309  cncms  23372  cnfldcusp  23374  resscdrg  23375  rrxprds  23398  ovoliunnul  23496  uniioombllem4  23575  vitalilem5  23601  mbfres  23631  ismbf3d  23641  i1fima  23665  i1fd  23668  itg2cnlem1  23748  itgss3  23801  ellimc2  23861  limccnp2  23876  cpnres  23920  lhop  23999  plyeq0  24187  plypf1  24188  sinhalfpilem  24436  sincos6thpi  24488  sincos3rdpi  24489  pige3  24490  dfrelog  24533  logimul  24581  logneg2  24582  dvlog  24618  cxpsqrt  24670  ang180lem2  24761  ang180lem3  24762  ang180lem4  24763  quart1  24804  asin1  24842  atan0  24856  atanlogsublem  24863  atan1  24876  log2tlbnd  24893  log2ublem2  24895  log2ub  24897  basellem8  25035  cht2  25119  ppiub  25150  bposlem6  25235  bposlem8  25237  bposlem9  25238  lgsdir2lem3  25273  lgseisenlem1  25321  lgseisenlem2  25322  lgsquadlem1  25326  lgsquadlem2  25327  2lgsoddprmlem2  25355  chebbnd1  25382  istrkg3ld  25581  tgcgr4  25647  motplusg  25658  ax5seglem7  26036  ex-un  27614  ex-sqrt  27644  ipdirilem  28015  ipasslem10  28025  hisubcomi  28292  normlem0  28297  norm3difi  28335  norm3lem  28337  polid2i  28345  chdmj1i  28671  chjjdiri  28714  spansn0  28731  pjoml4i  28777  cmbr3i  28790  qlaxr3i  28826  honpcani  29015  honpncani  29017  lnopunilem1  29200  lnophmlem2  29207  lnfn0i  29232  pjbdlni  29339  pjclem1  29385  pjclem3  29387  pjci  29390  atomli  29572  atabs2i  29592  mddmdin0i  29621  difeq  29684  disjdifprg  29717  imadifxp  29743  fnresin  29761  ofpreima2  29797  df1stres  29812  df2ndres  29813  cnvoprabOLD  29829  dfdec100  29907  decdiv10  29935  dpmul100  29936  dpmul1000  29938  dpexpp1  29947  dpadd2  29949  dpadd  29950  dpmul  29952  dpmul4  29953  threehalves  29954  xrge0base  30016  xrge00  30017  xrge0mulgnn0  30020  xrge0slmod  30175  lmatfvlem  30212  xrge0iifcnv  30310  lmxrge0  30329  cnrrext  30385  qqtopn  30386  esumrnmpt2  30461  esumpfinvallem  30467  unelldsys  30552  ldgenpisyslem1  30557  measunl  30610  mbfmcst  30652  difelcarsg  30703  carsggect  30711  sibfof  30733  eulerpartlemmf  30768  fib2  30795  fib3  30796  fib4  30797  fib5  30798  fib6  30799  0rrv  30844  coinfliprv  30875  ballotlem2  30881  prodfzo03  31012  chtvalz  31038  hgt750lemd  31057  hgt750lem  31060  hgt750lem2  31061  kur14lem6  31522  kur14lem7  31523  cvmlift2lem12  31625  problem5  31892  quad3  31893  divcnvlin  31947  logi  31949  bj-2upln1upl  33337  bj-rest0  33371  relowlssretop  33541  relowlpssretop  33542  1oequni2o  33546  curunc  33723  ptrest  33740  poimirlem16  33757  poimirlem30  33771  mblfinlem2  33779  ovoliunnfl  33783  voliunnfl  33785  itg2addnclem2  33794  ftc1anclem5  33821  ftc1anclem6  33822  sdc  33872  heiborlem3  33944  xrnresex  34506  dvh4dimN  37257  dnnumch1  38135  aomclem6  38150  areaquad  38323  unitadd  39019  seff  39029  sblpnf  39030  hashnzfz  39040  lhe4.4ex1a  39049  xrtgcntopre  40226  iccdifioo  40263  itgsin0pilem1  40687  stoweidlem13  40752  stoweidlem26  40765  fourierdlem62  40907  fourierdlem102  40947  fourierdlem114  40959  fourierswlem  40969  fouriersw  40970  sge0tsms  41119  meaiuninc  41220  fmtno4prmfac  42013  41prothprm  42065  2zrngasgrp  42469  2zrngmsgrp  42476  mvlraddi  43046  mvlrmuli  43055  i2linesi  43056
  Copyright terms: Public domain W3C validator