ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqeq1i GIF version

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

Proof of Theorem eqeq1i
StepHypRef Expression
1 eqeq1i.1 . 2 𝐴 = 𝐵
2 eqeq1 2196 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
31, 2ax-mp 5 1 (𝐴 = 𝐶𝐵 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wb 105   = wceq 1364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-cleq 2182
This theorem is referenced by:  ssequn2  3323  dfss1  3354  disj  3486  disjr  3487  undisj1  3495  undisj2  3496  uneqdifeqim  3523  reusn  3678  rabsneu  3680  eusn  3681  iin0r  4187  opeqsn  4270  unisuc  4431  onsucelsucexmid  4547  sucprcreg  4566  onintexmid  4590  dmopab3  4858  dm0rn0  4862  ssdmres  4947  imadisj  5008  args  5015  intirr  5033  dminxp  5091  dfrel3  5104  fntpg  5291  fncnv  5301  f0rn0  5429  dff1o4  5488  dffv4g  5531  fvun2  5604  fnreseql  5647  riota1  5871  riota2df  5873  fnotovb  5940  ovid  6014  ov  6017  ovg  6036  f1od2  6261  frec0g  6423  diffitest  6916  ismkvnex  7184  prarloclem5  7530  renegcl  8249  elznn0  9299  hashunlem  10819  maxclpr  11266  lgseisenlem1  14928  ex-ceil  14956  nninfsellemqall  15243  nninfomni  15247  iswomni0  15278
  Copyright terms: Public domain W3C validator