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

Theorem necon3bid 2296
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 2256 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3bid.1 . . 3 (𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))
32necon3bbid 2295 . 2 (𝜑 → (¬ 𝐴 = 𝐵𝐶𝐷))
41, 3syl5bb 190 1 (𝜑 → (𝐴𝐵𝐶𝐷))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 103   = wceq 1289  wne 2255
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580
This theorem depends on definitions:  df-bi 115  df-ne 2256
This theorem is referenced by:  nebidc  2335  addneintrd  7649  addneintr2d  7650  negne0bd  7765  negned  7769  subne0d  7781  subne0ad  7783  subneintrd  7816  subneintr2d  7818  qapne  9093  xrlttri3  9236  sqne0  9985  fihashneq0  10168  hashnncl  10169  cjne0  10307  absne0d  10585  sqrt2irraplemnn  11250
  Copyright terms: Public domain W3C validator