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

Theorem necon3bid 2381
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 2341 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3bid.1 . . 3 (𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))
32necon3bbid 2380 . 2 (𝜑 → (¬ 𝐴 = 𝐵𝐶𝐷))
41, 3syl5bb 191 1 (𝜑 → (𝐴𝐵𝐶𝐷))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 104   = wceq 1348  wne 2340
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 609  ax-in2 610
This theorem depends on definitions:  df-bi 116  df-ne 2341
This theorem is referenced by:  nebidc  2420  addneintrd  8107  addneintr2d  8108  negne0bd  8223  negned  8227  subne0d  8239  subne0ad  8241  subneintrd  8274  subneintr2d  8276  qapne  9598  xrlttri3  9754  xaddass2  9827  sqne0  10541  fihashneq0  10729  hashnncl  10730  cjne0  10872  absne0d  11151  sqrt2irraplemnn  12133  metn0  13172  lgsabs1  13734
  Copyright terms: Public domain W3C validator