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

Theorem necon3bid 2388
Description: Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon3bid.1 (𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))
Assertion
Ref Expression
necon3bid (𝜑 → (𝐴𝐵𝐶𝐷))

Proof of Theorem necon3bid
StepHypRef Expression
1 df-ne 2348 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3bid.1 . . 3 (𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))
32necon3bbid 2387 . 2 (𝜑 → (¬ 𝐴 = 𝐵𝐶𝐷))
41, 3bitrid 192 1 (𝜑 → (𝐴𝐵𝐶𝐷))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 105   = wceq 1353  wne 2347
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 614  ax-in2 615
This theorem depends on definitions:  df-bi 117  df-ne 2348
This theorem is referenced by:  nebidc  2427  addneintrd  8143  addneintr2d  8144  negne0bd  8259  negned  8263  subne0d  8275  subne0ad  8277  subneintrd  8310  subneintr2d  8312  qapne  9637  xrlttri3  9795  xaddass2  9868  sqne0  10582  fihashneq0  10769  hashnncl  10770  cjne0  10912  absne0d  11191  sqrt2irraplemnn  12173  ringinvnz1ne0  13179  metn0  13771  lgsabs1  14333  neap0mkv  14698
  Copyright terms: Public domain W3C validator