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

Theorem eqeq1i 2806
Description: Inference from equality to equivalence of equalities. (Contributed by NM, 15-Jul-1993.)
Hypothesis
Ref Expression
eqeq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
eqeq1i (𝐴 = 𝐶𝐵 = 𝐶)

Proof of Theorem eqeq1i
StepHypRef Expression
1 eqeq1i.1 . 2 𝐴 = 𝐵
2 eqeq1 2805 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
31, 2ax-mp 5 1 (𝐴 = 𝐶𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794
This theorem is referenced by:  eqeq12i  2816  neeq1i  3054  ssequn2  4113  sseqin2  4145  dfss7  4170  dfss4  4188  rabeq0  4295  disj  4358  disjOLD  4359  disjr  4360  undisj1  4372  undisj2  4373  undif  4391  uneqdifeq  4399  rabeqsn  4569  reusn  4626  rabsneu  4628  eusn  4629  tppreqb  4701  elpreqpr  4760  uniintsn  4878  iin0  5229  dfepfr  5508  epfrc  5509  dmopab3  5756  dm0rn0  5763  ssdmres  5845  iresn0n0  5894  imadisj  5919  args  5928  dffr3  5933  intirr  5949  dminxp  6008  dfrel3  6026  coeq0  6079  sspred  6128  dffr4  6136  tz6.26  6151  wfi  6153  unisuc  6239  fntpg  6388  fncnv  6401  mptfnf  6459  sbcfng  6488  f0rn0  6542  dff1o4  6602  dffv4  6646  fvun2  6734  fnreseql  6799  funopdmsn  6893  riota1  7118  riota2df  7120  riotaeqimp  7123  fnbrovb  7188  ovid  7274  ov  7277  ovg  7297  ovima0  7311  opiota  7743  wfrlem8  7949  tz7.49c  8069  sucprcreg  9053  zfregfr  9056  inf3lem2  9080  zfregs2  9163  rankxpsuc  9299  scott0s  9305  cplem1  9306  cfslb2n  9683  fin23lem26  9740  dfacfin7  9814  axdc3lem4  9868  zorn2lem7  9917  alephom  10000  fpwwe2  10058  recmulnq  10379  recexsr  10522  map2psrpr  10525  renegcli  10940  addeq0  11056  elznn0  11988  xrsupss  12694  xrinfmss  12695  prinfzo0  13075  seqf1olem1  13409  seqf1olem2  13410  sqeqori  13576  hashrabsn1  13735  hashprb  13758  hashprdifel  13759  hashbclem  13810  hash2pwpr  13834  f1oun2prg  14274  modfsummods  15143  cshwrepswhash1  16431  ismgmid  17870  smndex2dnrinv  18075  oppgid  18479  lsmdisjr  18805  gexex  18969  gsumxp2  19096  dprd0  19149  oppr1  19383  opprunit  19410  opprdomn  20070  zringndrg  20186  gsummoncoe1  20936  mat0dimcrng  21078  iinopn  21510  elcls  21681  ordthaus  21992  hauscmplem  22014  regr1lem2  22348  metdseq0  23462  minveclem1  24031  minveclem3b  24035  volun  24152  dyaddisj  24203  vieta1  24911  logeftb  25178  birthdaylem1  25540  dmgmaddn0  25611  gausslemma2d  25961  lgseisenlem1  25962  2lgslem4  25993  rpvmasum  26113  axsegconlem6  26719  edg0iedg0  26851  numedglnl  26940  ushgredgedg  27022  ushgredgedgloop  27024  uhgr0v0e  27031  usgr1v0edg  27050  usgrexmpllem  27053  usgr1v0e  27119  nbuhgr2vtx1edgblem  27144  uvtx01vtx  27190  prcliscplgr  27207  cusgr0v  27221  vtxdg0e  27267  1loopgrvd2  27296  finsumvtxdg2ssteplem4  27341  finsumvtxdg2size  27343  isrgr  27352  fusgrregdegfi  27362  wspn0  27713  2wlkdlem8  27722  3wlkdlem8  27955  uhgr3cyclexlem  27969  1to2vfriswmgr  28067  1to3vfriswmgr  28068  frgrregorufr0  28112  frgrreg  28182  frgrregord013  28183  ex-ceil  28236  nmlno0lem  28579  minvecolem1  28660  hvsubeq0i  28849  hvsubaddi  28852  pjoc2i  29224  pjoml3i  29372  cmbr3i  29386  pjss2i  29466  hosubeq0i  29612  dmadjrnb  29692  nmlnop0iALT  29781  nmopcoadj0i  29889  stm1ri  30030  jplem2  30055  atoml2i  30169  chirredlem1  30176  cdj3lem3  30224  difininv  30291  undifr  30299  disjnf  30336  disjpreima  30350  disjunsn  30360  f1od2  30486  wrdt2ind  30656  zrhchr  31325  ddemeas  31603  braew  31609  aean  31611  eulerpartlemgh  31744  ballotlemfp1  31857  repr0  31990  hgt750lem2  32031  bnj1143  32170  acycgr0v  32503  prclisacycgr  32506  cvmsss2  32629  cvmlift2lem13  32670  elrn3  33106  frpomin2  33187  frpoind  33188  frind  33193  frrlem13  33243  sltsolem1  33288  madeval2  33398  rankeq1o  33740  hfun  33747  bj-disj2r  34459  bj-sscon  34460  bj-0int  34511  bj-imdirco  34600  bj-pinftynminfty  34637  finxpreclem4  34806  nlpineqsn  34820  curunc  35032  tan2h  35042  poimirlem13  35063  poimirlem14  35064  poimirlem21  35071  poimirlem22  35072  asindmre  35133  totbndbnd  35220  rngosn3  35355  scott0f  35600  ineqcom  35657  n0el2  35743  dfrel5  35756  dfrel6  35757  redundeq1  36017  dmqscoelseq  36048  dfeldisj5  36107  atbase  36578  llnbase  36798  lplnbase  36823  lvolbase  36867  lhpbase  37287  cdlemg31b0N  37983  cdlemg31b0a  37984  cdlemh  38106  metakunt24  39364  iunrelexp0  40390  frege120  40671  clsk1indlem4  40734  gneispace  40824  scotteld  40941  undisjrab  40997  zfregs2VD  41534  dvnprod  42578  fnresfnco  43620  aiotavb  43634  afvpcfv0  43689  aovpcov0  43733  aov0ov0  43736  aovov0bi  43739  fnotaovb  43741  funressndmafv2rn  43766  fmtnoprmfac1lem  44068  lighneallem2  44111  snlindsntor  44867  rrx2pnedifcoorneorr  45118  itschlc0xyqsol1  45167  2itscp  45182
  Copyright terms: Public domain W3C validator