![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > necon2ad | GIF version |
Description: Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.) |
Ref | Expression |
---|---|
necon2ad.1 | ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) |
Ref | Expression |
---|---|
necon2ad | ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon2ad.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) | |
2 | 1 | con2d 625 | . 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: 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 |