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

Theorem eqtr3i 2454
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 2436 . 2  |-  B  =  A
3 eqtr3i.2 . 2  |-  A  =  C
42, 3eqtri 2452 1  |-  B  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1438
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-cleq 2415
This theorem is referenced by:  3eqtr3i  2460  3eqtr3ri  2461  unundi  3628  unundir  3629  inindi  3680  inindir  3681  dfin4  3714  difun1  3734  difabs  3738  notab  3744  dif0  3866  difdifdir  3884  tpidm13  4100  tpprceq3  4138  intmin2  4281  univ  4670  iunxpconst  4908  dmres  5142  opabresid  5175  rnresi  5198  cnvcnv  5305  rnresv  5312  cnvsn0  5321  cnvsn  5336  resdmres  5343  coi2  5369  coires1  5370  dfdm2  5385  isarep2  5679  resasplit  5768  ssimaex  5944  fnreseql  6005  resfunexg  6143  idref  6159  mpt2mpt  6400  caov31  6510  fvresex  6778  xpexgALT  6798  1st2val  6831  2nd2val  6832  fnsuppeq0  6952  ecopovtrn  7472  limensuci  7752  pssnn  7794  r1sucg  8243  jech9.3  8288  rankbnd2  8343  compss  8808  zorn2lem4  8931  iunfo  8966  cardf  8977  alephsuc3  9007  fpwwe2lem13  9069  rankcf  9204  halfnq  9403  addclprlem2  9444  mulgt0sr  9531  mul02lem2  9812  mul02  9813  addid1  9815  mvlladdi  9894  mvllmuli  10442  infrenegsup  10593  infmsupOLD  10594  8th4div3  10835  nneo  11021  dec10  11083  nummac  11085  numadd  11087  numaddc  11088  nummul1c  11089  9p2e11  11115  decbin0  11156  rpsup  12094  resup  12095  om2uzrdg  12171  m1expcl2  12295  facnn  12462  fac0  12463  faclbnd4lem1  12479  4bc3eq4  12514  hasheq0  12545  f1oun2prg  12996  sqrt1  13329  sqrt4  13330  sqrt9  13331  rddif  13397  abs3lemi  13466  sumss2  13785  divcnvshft  13906  geo2sum2  13923  geomulcvg  13925  geoihalfsum  13931  risefall0lem  14072  bpoly2  14103  bpoly3  14104  sin0  14196  efival  14199  ef01bndlem  14231  cos2bnd  14235  sin4lt0  14242  2prm  14633  unbenlem  14845  dec5dvds  15029  modxai  15033  mod2xi  15034  mod2xnegi  15036  gcdi  15038  numexp2x  15044  decsplit  15048  setsid  15157  mreexexlem3d  15545  oppchom  15613  2oppchomf  15622  isoval  15663  estrres  16017  oppchofcl  16138  oyoncl  16148  mvdco  17079  m1expaddsub  17132  psgn0fv0  17145  oppglsm  17287  dprd2da  17668  ring1  17823  opprsubg  17857  lsppratlem1  18363  opsrtoslem1  18700  ply1basfvi  18827  coe1tm  18859  ply1coe  18882  ply1coeOLD  18883  zzngim  19115  cnmsgnsubg  19137  psgninv  19142  zrhpsgnmhm  19144  neitr  20188  comppfsc  20539  kgeni  20544  xkoinjcn  20694  ufprim  20916  metreslem  21369  restmetu  21577  retopbas  21773  cnfldms  21788  qdensere2  21807  xrsmopn  21822  metdscn2  21866  metdscn2OLD  21881  pcoass  22047  iscmet3lem3  22252  cncms  22314  cnfldcusp  22316  resscdrg  22317  rrxprds  22340  ovoliunnul  22452  uniioombllem4  22536  vitalilem5  22562  mbfres  22592  ismbf3d  22602  i1fima  22628  i1fd  22631  itg2cnlem1  22711  itgss3  22764  ellimc2  22824  limccnp2  22839  cpnres  22883  lhop  22960  plyeq0  23157  plypf1  23158  sinhalfpilem  23410  sincos6thpi  23462  sincos3rdpi  23463  pige3  23464  dfrelog  23507  logimul  23555  logneg2  23556  dvlog  23588  cxpsqrt  23640  ang180lem2  23731  ang180lem3  23732  ang180lem4  23733  quart1  23774  asin1  23812  atan0  23826  atanlogsublem  23833  atan1  23846  log2tlbnd  23863  log2ublem2  23865  log2ub  23867  basellem8  24006  cht2  24091  ppiub  24124  bposlem6  24209  bposlem8  24211  bposlem9  24212  lgsdir2lem3  24245  lgseisenlem1  24269  lgseisenlem2  24270  lgsquadlem1  24274  lgsquadlem2  24275  chebbnd1  24302  istrkg3ld  24501  tgcgr4  24568  motplusg  24579  ax5seglem7  24957  ex-un  25866  circgrpOLD  26094  ipdirilem  26462  ipasslem10  26472  hisubcomi  26749  normlem0  26754  norm3difi  26792  norm3lem  26794  polid2i  26802  chdmj1i  27126  chjjdiri  27169  spansn0  27186  pjoml4i  27232  cmbr3i  27245  qlaxr3i  27281  honpcani  27470  honpncani  27472  lnopunilem1  27655  lnophmlem2  27662  lnfn0i  27687  pjbdlni  27794  pjclem1  27840  pjclem3  27842  pjci  27845  atomli  28027  atabs2i  28047  mddmdin0i  28076  difeq  28144  iunxdif3  28171  disjdifprg  28181  imadifxp  28208  fnresin  28224  ofpreima2  28265  df1stres  28280  df2ndres  28281  cnvoprab  28308  xrge0base  28448  xrge00  28449  xrge0mulgnn0  28452  xrge0slmod  28609  lmatfvlem  28643  ordtconlem1  28732  xrge0iifcnv  28741  lmxrge0  28760  cnrrext  28816  qqtopn  28817  esumrnmpt2  28891  esumpfinvallem  28897  unelldsys  28982  ldgenpisyslem1  28987  measvuni  29038  measunl  29040  measinb  29045  mbfmcst  29083  difelcarsg  29144  carsggect  29152  sibfof  29175  eulerpartlemmf  29210  fib2  29237  fib3  29238  fib4  29239  fib5  29240  fib6  29241  0rrv  29286  coinfliprv  29317  ballotlem2  29323  ballotlemgun  29359  ballotlemgunOLD  29397  kur14lem6  29936  kur14lem7  29937  cvmlift2lem12  30039  problem5  30303  quad3  30304  divcnvlin  30368  logi  30371  bj-2upln1upl  31580  relowlssretop  31713  relowlpssretop  31714  ptrest  31859  poimirlem16  31876  poimirlem30  31890  mblfinlem2  31898  ovoliunnfl  31902  voliunnfl  31904  itg2addnclem2  31914  ftc1anclem5  31941  ftc1anclem6  31942  sdc  31993  heiborlem3  32065  dvh4dimN  34940  dnnumch1  35828  aomclem6  35843  areaquad  36027  unitadd  36506  seff  36521  sblpnf  36522  hashnzfz  36533  lhe4.4ex1a  36542  iccdifioo  37453  itgsin0pilem1  37652  stoweidlem13  37699  stoweidlem26  37712  fourierdlem62  37858  fourierdlem102  37898  fourierdlem114  37910  fourierswlem  37920  fouriersw  37921  sge0tsms  38016  41prothprm  38637  2zrngasgrp  39244  2zrngmsgrp  39251  mvlraddi  39810  mvlrmuli  39822  i2linesi  39823
  Copyright terms: Public domain W3C validator