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

Theorem necon2ad 2417
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 625 . 2 (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
3 df-ne 2361 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
42, 3imbitrrdi 162 1 (𝜑 → (𝜓𝐴𝐵))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1364  wne 2360
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616
This theorem depends on definitions:  df-bi 117  df-ne 2361
This theorem is referenced by:  necon2d  2419  prneimg  3789  tz7.2  4372  nordeq  4561  pr2ne  7222  ltne  8073  apne  8611  xrltne  9845  npnflt  9847  nmnfgt  9850  ge0nemnf  9856  rpexp  12188  sqrt2irr  12197  pcgcd1  12363  nzrunit  13552  lgsmod  14905
  Copyright terms: Public domain W3C validator