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

Theorem necon2ad 2397
Description: Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
Hypothesis
Ref Expression
necon2ad.1 (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
Assertion
Ref Expression
necon2ad (𝜑 → (𝜓𝐴𝐵))

Proof of Theorem necon2ad
StepHypRef Expression
1 necon2ad.1 . . 3 (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
21con2d 619 . 2 (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
3 df-ne 2341 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
42, 3syl6ibr 161 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   = 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:  necon2d  2399  prneimg  3761  tz7.2  4339  nordeq  4528  pr2ne  7169  ltne  8004  apne  8542  xrltne  9770  npnflt  9772  nmnfgt  9775  ge0nemnf  9781  rpexp  12107  sqrt2irr  12116  pcgcd1  12281  lgsmod  13721
  Copyright terms: Public domain W3C validator