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

Theorem necon3bd 2403
Description: Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
Hypothesis
Ref Expression
necon3bd.1 (𝜑 → (𝐴 = 𝐵𝜓))
Assertion
Ref Expression
necon3bd (𝜑 → (¬ 𝜓𝐴𝐵))

Proof of Theorem necon3bd
StepHypRef Expression
1 necon3bd.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
21con3d 632 . 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:  nelne1  2450  nelne2  2451  nssne1  3228  nssne2  3229  disjne  3491  difsn  3744  nbrne1  4037  nbrne2  4038  ac6sfi  6927  indpi  7372  zneo  9385  pc2dvds  12365  pcadd  12375  oddprmdvds  12389  4sqlem11  12436  lssvneln0  13706  lgsne0  14917
  Copyright terms: Public domain W3C validator