![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > necon3bd | GIF version |
Description: Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.) |
Ref | Expression |
---|---|
necon3bd.1 | ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) |
Ref | Expression |
---|---|
necon3bd | ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3bd.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) | |
2 | 1 | con3d 632 | . 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝐴 = 𝐵)) |
3 | df-ne 2361 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
4 | 2, 3 | imbitrrdi 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 |