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

Theorem neeq1 2370
Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
Assertion
Ref Expression
neeq1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))

Proof of Theorem neeq1
StepHypRef Expression
1 eqeq1 2194 . . 3 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
21notbid 668 . 2 (𝐴 = 𝐵 → (¬ 𝐴 = 𝐶 ↔ ¬ 𝐵 = 𝐶))
3 df-ne 2358 . 2 (𝐴𝐶 ↔ ¬ 𝐴 = 𝐶)
4 df-ne 2358 . 2 (𝐵𝐶 ↔ ¬ 𝐵 = 𝐶)
52, 3, 43bitr4g 223 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 105   = wceq 1363  wne 2357
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-in1 615  ax-in2 616  ax-5 1457  ax-gen 1459  ax-4 1520  ax-17 1536  ax-ext 2169
This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-ne 2358
This theorem is referenced by:  neeq1i  2372  neeq1d  2375  nelrdva  2956  disji2  4008  0inp0  4178  frecabcl  6414  fiintim  6942  eldju2ndl  7085  updjudhf  7092  netap  7267  2oneel  7269  2omotaplemap  7270  2omotaplemst  7271  exmidapne  7273  xnn0nemnf  9264  uzn0  9557  xrnemnf  9791  xrnepnf  9792  ngtmnft  9831  xsubge0  9895  xposdif  9896  xleaddadd  9901  fztpval  10097  pcpre1  12306  pcqmul  12317  pcqcl  12320  xpsfrnel  12782  fiinopn  13857  neapmkv  15170  neap0mkv  15171  ltlenmkv  15172
  Copyright terms: Public domain W3C validator