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

Theorem eqeq1i 2614
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 2613 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
31, 2ax-mp 5 1 (𝐴 = 𝐶𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602
This theorem is referenced by:  eqeq12i  2623  neeq1i  2845  ssequn2  3747  sseqin2  3778  dfss1OLD  3779  dfss4  3819  rabeq0  3910  disj  3968  disjr  3969  undisj1  3980  undisj2  3981  undif  4000  uneqdifeq  4008  uneqdifeqOLD  4009  reusn  4205  rabsneu  4207  eusn  4208  tppreqb  4276  elpreqpr  4329  uniintsn  4443  iin0  4759  opeqsn  4885  dfepfr  5012  epfrc  5013  dmopab3  5245  dm0rn0  5249  ssdmres  5326  imadisj  5389  args  5398  dffr3  5403  intirr  5419  dminxp  5478  dfrel3  5495  coeq0  5546  sspred  5590  dffr4  5598  tz6.26  5613  wfi  5615  unisuc  5703  fntpg  5847  fncnv  5861  mptfnf  5913  sbcfng  5940  f0rn0  5987  dff1o4  6042  dffv4  6084  fvun2  6164  fnreseql  6219  riota1  6506  riota2df  6508  fnotovb  6569  ovid  6652  ov  6655  ovg  6674  ovima0  6688  opiota  7095  wfrlem8  7286  tz7.49c  7405  sucprcreg  8366  zfregfr  8369  inf3lem2  8386  zfregs2  8469  rankxpsuc  8605  scott0s  8611  cplem1  8612  cfslb2n  8950  fin23lem26  9007  dfacfin7  9081  axdc3lem4  9135  zorn2lem7  9184  alephom  9263  fpwwe2  9321  recmulnq  9642  recexsr  9784  map2psrpr  9787  renegcli  10193  elznn0  11227  xrsupss  11969  xrinfmss  11970  seqf1olem1  12659  seqf1olem2  12660  sqeqori  12795  hashrabsn1  12978  hashprb  13000  hashprdifel  13001  hashbclem  13047  hash2pwpr  13067  swrdccat3a  13293  f1oun2prg  13460  modfsummods  14314  cshwrepswhash1  15595  ismgmid  17035  oppgid  17557  lsmdisjr  17868  gexex  18027  dprd0  18201  oppr1  18405  opprunit  18432  opprdomn  19070  gsummoncoe1  19443  mat0dimcrng  20042  iinopn  20479  elcls  20634  ordthaus  20945  hauscmplem  20966  regr1lem2  21300  metdseq0  22412  minveclem1  22947  minveclem3b  22951  volun  23064  dyaddisj  23114  vieta1  23815  logeftb  24078  birthdaylem1  24422  dmgmaddn0  24493  gausslemma2d  24843  lgseisenlem1  24844  2lgslem4  24875  rpvmasum  24959  axsegconlem6  25547  usgraedgprv  25698  wlkdvspthlem  25930  wlknwwlknsur  26033  wlkiswwlksur  26040  clwlkfclwwlk1hashn  26161  clwlkfoclwwlk  26165  1to3vfriswmgra  26327  frgrawopreg2  26371  ex-ceil  26490  nmlno0lem  26825  minvecolem1  26907  hvsubeq0i  27097  hvsubaddi  27100  pjoc2i  27474  pjoml3i  27622  cmbr3i  27636  pjss2i  27716  hosubeq0i  27862  dmadjrnb  27942  nmlnop0iALT  28031  nmopcoadj0i  28139  stm1ri  28280  jplem2  28305  atoml2i  28419  chirredlem1  28426  cdj3lem3  28474  disjnf  28559  disjpreima  28572  disjunsn  28582  f1od2  28680  addeq0  28691  zrhchr  29141  ddemeas  29419  braew  29425  aean  29427  eulerpartlemgh  29560  ballotlemfp1  29673  bnj1143  29908  cvmsss2  30303  cvmlift2lem13  30344  elrn3  30699  br1steq  30710  br2ndeq  30711  frind  30777  sltsolem1  30860  rankeq1o  31241  hfun  31248  bj-pinftynminfty  32074  finxpreclem4  32190  curunc  32344  tan2h  32354  poimirlem13  32375  poimirlem14  32376  poimirlem21  32383  poimirlem22  32384  asindmre  32448  totbndbnd  32541  rngosn3  32676  scott0f  32930  atbase  33377  llnbase  33596  lplnbase  33621  lvolbase  33665  lhpbase  34085  cdlemg31b0N  34783  cdlemg31b0a  34784  cdlemh  34906  iunrelexp0  36796  frege120  37080  clsk1indlem4  37145  gneispace  37235  undisjrab  37310  zfregs2VD  37881  dvnprod  38622  fnresfnco  39638  afvpcfv0  39659  aovpcov0  39703  aov0ov0  39706  aovov0bi  39709  fnotaovb  39711  fmtnoprmfac1lem  39798  lighneallem2  39845  riotaeqimp  40144  prinfzo0  40169  ushgredgedga  40437  ushgredgedgaloop  40439  uhgr0v0e  40445  usgrexmpllem  40465  usgr1v0e  40526  nbuhgr2vtx1edgblem  40554  uvtxa01vtx0  40604  uvtxa01vtx  40605  cusgr0v  40631  vtxdg0e  40670  1loopgrvd2  40699  isrgr  40740  fusgrregdegfi  40750  wlknwwlksnsur  41068  wlkwwlksur  41075  21wlkdlem8  41121  clwlksfclwwlk1hashn  41247  clwlksfoclwwlk  41251  31wlkdlem8  41315  uhgr3cyclexlem  41329  1to2vfriswmgr  41430  1to3vfriswmgr  41431  frgrwopreg2  41469  av-frgrareg  41529  av-frgraregord013  41530  snlindsntor  42035
  Copyright terms: Public domain W3C validator