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

Theorem necon3bid 2368
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 2328 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3bid.1 . . 3 (𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))
32necon3bbid 2367 . 2 (𝜑 → (¬ 𝐴 = 𝐵𝐶𝐷))
41, 3syl5bb 191 1 (𝜑 → (𝐴𝐵𝐶𝐷))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 104   = wceq 1335  wne 2327
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 604  ax-in2 605
This theorem depends on definitions:  df-bi 116  df-ne 2328
This theorem is referenced by:  nebidc  2407  addneintrd  8063  addneintr2d  8064  negne0bd  8179  negned  8183  subne0d  8195  subne0ad  8197  subneintrd  8230  subneintr2d  8232  qapne  9548  xrlttri3  9704  xaddass2  9774  sqne0  10484  fihashneq0  10669  hashnncl  10670  cjne0  10808  absne0d  11087  sqrt2irraplemnn  12054  metn0  12789
  Copyright terms: Public domain W3C validator