| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > necon3ai | Structured version Visualization version GIF version | ||
| Description: Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 28-Oct-2024.) |
| Ref | Expression |
|---|---|
| necon3ai.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| necon3ai | ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | neneq 2946 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵) | |
| 2 | necon3ai.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 3 | 1, 2 | nsyl 140 | 1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1540 ≠ wne 2940 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-ne 2941 |
| This theorem is referenced by: necon1ai 2968 necon3i 2973 neneor 3042 nelsn 4666 disjsn2 4712 prnesn 4860 opelopabsb 5535 funsndifnop 7171 ord1eln01 8534 map0b 8923 mapdom3 9189 cflim2 10303 isfin4p1 10355 fpwwe2lem12 10682 tskuni 10823 recextlem2 11894 hashprg 14434 eqsqrt2d 15407 gcd1 16565 gcdzeq 16589 lcmfunsnlem2lem1 16675 lcmfunsnlem2lem2 16676 phimullem 16816 pcgcd1 16915 pc2dvds 16917 pockthlem 16943 ablfacrplem 20085 znrrg 21584 opnfbas 23850 supfil 23903 itg1addlem4 25734 itg1addlem5 25735 mpodvdsmulf1o 27237 dvdsmulf1o 27239 ppiub 27248 dchrelbas4 27287 2sqlem8 27470 tgldimor 28510 subfacp1lem6 35190 cvmsss2 35279 ax6e2ndeq 44579 supminfxr2 45480 fourierdlem56 46177 ichnreuop 47459 |
| Copyright terms: Public domain | W3C validator |