![]() |
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 2950 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵) | |
2 | necon3ai.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
3 | 1, 2 | nsyl 140 | 1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1542 ≠ wne 2944 |
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 206 df-ne 2945 |
This theorem is referenced by: necon1ai 2972 necon3i 2977 neneor 3045 nelsn 4627 disjsn2 4674 prnesn 4818 opelopabsb 5488 funsndifnop 7098 ord1eln01 8443 map0b 8822 mapdom3 9094 cflim2 10200 isfin4p1 10252 fpwwe2lem12 10579 tskuni 10720 recextlem2 11787 hashprg 14296 eqsqrt2d 15254 gcd1 16409 gcdzeq 16434 lcmfunsnlem2lem1 16515 lcmfunsnlem2lem2 16516 phimullem 16652 pcgcd1 16750 pc2dvds 16752 pockthlem 16778 ablfacrplem 19845 znrrg 20975 opnfbas 23196 supfil 23249 itg1addlem4 25066 itg1addlem4OLD 25067 itg1addlem5 25068 dvdsmulf1o 26546 ppiub 26555 dchrelbas4 26594 2sqlem8 26777 tgldimor 27447 subfacp1lem6 33782 cvmsss2 33871 ax6e2ndeq 42848 supminfxr2 43711 fourierdlem56 44410 ichnreuop 45671 |
Copyright terms: Public domain | W3C validator |