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

Theorem eqeq1i 2125
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 2124 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
31, 2ax-mp 5 1 (𝐴 = 𝐶𝐵 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wb 104   = wceq 1316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  ssequn2  3219  dfss1  3250  disj  3381  disjr  3382  undisj1  3390  undisj2  3391  uneqdifeqim  3418  reusn  3564  rabsneu  3566  eusn  3567  iin0r  4063  opeqsn  4144  unisuc  4305  onsucelsucexmid  4415  sucprcreg  4434  onintexmid  4457  dmopab3  4722  dm0rn0  4726  ssdmres  4811  imadisj  4871  args  4878  intirr  4895  dminxp  4953  dfrel3  4966  fntpg  5149  fncnv  5159  f0rn0  5287  dff1o4  5343  dffv4g  5386  fvun2  5456  fnreseql  5498  riota1  5716  riota2df  5718  fnotovb  5782  ovid  5855  ov  5858  ovg  5877  f1od2  6100  frec0g  6262  diffitest  6749  ismkvnex  6997  prarloclem5  7276  renegcl  7991  elznn0  9037  hashunlem  10518  maxclpr  10962  ex-ceil  12865  nninfsellemqall  13138  nninfomni  13142
  Copyright terms: Public domain W3C validator