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  8147  addneintr2d  8148  negne0bd  8263  negned  8267  subne0d  8279  subne0ad  8281  subneintrd  8314  subneintr2d  8316  qapne  9641  xrlttri3  9799  xaddass2  9872  sqne0  10588  fihashneq0  10776  hashnncl  10777  cjne0  10919  absne0d  11198  sqrt2irraplemnn  12181  ringinvnz1ne0  13231  metn0  13917  lgsabs1  14479  neap0mkv  14856
  Copyright terms: Public domain W3C validator