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  8145  addneintr2d  8146  negne0bd  8261  negned  8265  subne0d  8277  subne0ad  8279  subneintrd  8312  subneintr2d  8314  qapne  9639  xrlttri3  9797  xaddass2  9870  sqne0  10586  fihashneq0  10774  hashnncl  10775  cjne0  10917  absne0d  11196  sqrt2irraplemnn  12179  ringinvnz1ne0  13226  metn0  13881  lgsabs1  14443  neap0mkv  14819
  Copyright terms: Public domain W3C validator