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

Theorem necon3bid 2349
 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 2309 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3bid.1 . . 3 (𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))
32necon3bbid 2348 . 2 (𝜑 → (¬ 𝐴 = 𝐵𝐶𝐷))
41, 3syl5bb 191 1 (𝜑 → (𝐴𝐵𝐶𝐷))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104   = wceq 1331   ≠ wne 2308 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604 This theorem depends on definitions:  df-bi 116  df-ne 2309 This theorem is referenced by:  nebidc  2388  addneintrd  7950  addneintr2d  7951  negne0bd  8066  negned  8070  subne0d  8082  subne0ad  8084  subneintrd  8117  subneintr2d  8119  qapne  9431  xrlttri3  9583  xaddass2  9653  sqne0  10358  fihashneq0  10541  hashnncl  10542  cjne0  10680  absne0d  10959  sqrt2irraplemnn  11857  metn0  12547
 Copyright terms: Public domain W3C validator