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

Theorem eqeq1i 2063
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 2062 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
31, 2ax-mp 7 1 (𝐴 = 𝐶𝐵 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wb 102   = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  ssequn2  3144  dfss1  3169  disj  3296  disjr  3297  undisj1  3307  undisj2  3308  uneqdifeqim  3336  reusn  3469  rabsneu  3471  eusn  3472  iin0r  3950  opeqsn  4017  unisuc  4178  onsucelsucexmid  4283  sucprcreg  4301  onintexmid  4325  dmopab3  4576  dm0rn0  4580  ssdmres  4661  imadisj  4715  args  4722  intirr  4739  dminxp  4793  dfrel3  4806  fntpg  4983  fncnv  4993  dff1o4  5162  dffv4g  5203  fvun2  5268  fnreseql  5305  riota1  5514  riota2df  5516  fnotovb  5576  ovid  5645  ov  5648  ovg  5667  f1od2  5884  frec0g  6014  diffitest  6375  prarloclem5  6656  renegcl  7335  elznn0  8317  ex-ceil  10280
  Copyright terms: Public domain W3C validator