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

Theorem eqeq1i 2464
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 2461 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  =wceq 1395
This theorem is referenced by:  eqeq12i  2477  neeq1i  2742  ssequn2  3676  dfss1  3702  dfss4  3731  disj  3867  disjr  3868  undisj1  3878  undisj2  3879  undif  3908  uneqdifeq  3916  reusn  4103  rabsneu  4105  eusn  4106  tppreqb  4171  uniintsn  4324  iin0  4626  opeqsn  4748  dfepfr  4869  epfrc  4870  unisuc  4959  dmopab3  5220  dm0rn0  5224  ssdmres  5300  imadisj  5361  args  5370  dffr3  5374  intirr  5390  dminxp  5452  dfrel3  5469  coeq0  5521  fntpg  5648  fncnv  5657  sbcfng  5733  f0rn0  5775  dff1o4  5829  dffv4  5868  fvun2  5945  fnreseql  5997  riota1  6276  riota2df  6278  fnotovb  6338  ovid  6419  ov  6422  ovg  6441  ovima0  6454  opiota  6859  tz7.49c  7130  sucprcreg  8046  sucprcregOLD  8047  inf3lem2  8067  zfregs2  8185  rankxpsuc  8321  scott0s  8327  cplem1  8328  cfslb2n  8669  fin23lem26  8726  dfacfin7  8800  axdc3lem4  8854  zorn2lem7  8903  alephom  8981  fpwwe2  9042  recmulnq  9363  recexsr  9505  map2psrpr  9508  renegcli  9903  elznn0  10904  xrsupss  11529  xrinfmss  11530  seqf1olem1  12146  seqf1olem2  12147  sqeqori  12280  hashrabsn1  12442  hashprb  12462  hashprdifel  12463  hashbclem  12501  hash2pwpr  12519  swrdccat3a  12719  f1oun2prg  12865  modfsummods  13607  cshwrepswhash1  14587  ismgmid  15891  oppgid  16391  lsmdisjr  16702  gexex  16859  dprd0  17078  oppr1  17283  opprunit  17310  opprdomn  17950  gsummoncoe1  18346  mat0dimcrng  18972  iinopn  19411  elcls  19574  ordthaus  19885  hauscmplem  19906  regr1lem2  20241  metdseq0  21358  minveclem1  21839  minveclem3b  21843  volun  21955  dyaddisj  22005  vieta1  22708  logeftb  22968  birthdaylem1  23281  lgseisenlem1  23624  rpvmasum  23711  axsegconlem6  24225  usgraedgprv  24376  wlkdvspthlem  24609  wlknwwlknsur  24712  wlkiswwlksur  24719  clwlkfclwwlk1hashn  24841  clwlkfoclwwlk  24845  1to3vfriswmgra  25007  frgrawopreg2  25051  rngosn3  25428  nmlno0lem  25708  minvecolem1  25790  hvsubeq0i  25980  hvsubaddi  25983  pjoc2i  26356  pjoml3i  26504  cmbr3i  26518  pjss2i  26598  hosubeq0i  26745  dmadjrnb  26825  nmlnop0iALT  26914  nmopcoadj0i  27022  stm1ri  27163  jplem2  27188  atoml2i  27302  chirredlem1  27309  cdj3lem3  27357  disjnf  27433  disjpreima  27445  disjunsn  27453  mptfnf  27499  f1od2  27547  addeq0  27558  zrhchr  27957  ddemeas  28208  braew  28214  aean  28216  eulerpartlemgh  28317  ballotlemfp1  28430  dmgmaddn0  28565  cvmsss2  28719  cvmlift2lem13  28760  elrn3  29192  br1steq  29204  br2ndeq  29205  sspred  29252  dffr4  29262  tz6.26  29285  wfi  29287  frind  29323  wfrlem8  29350  sltsolem1  29428  rankeq1o  29828  hfun  29835  tan2h  30047  asindmre  30102  totbndbnd  30285  scott0f  30577  undisjrab  31186  dvnprod  31746  fnresfnco  32211  afvpcfv0  32231  aovpcov0  32275  aov0ov0  32278  aovov0bi  32281  fnotaovb  32283  usgo0s0ALT  32436  usgo1s0ALT  32437  snlindsntor  33072  zfregs2VD  33641  bnj1143  33849  bj-pinftynminfty  34630  atbase  35014  llnbase  35233  lplnbase  35258  lvolbase  35302  lhpbase  35722  cdlemg31b0N  36420  cdlemg31b0a  36421  cdlemh  36543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449
  Copyright terms: Public domain W3C validator