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.) |
Ref | Expression |
---|---|
necon3ai.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
necon3ai | ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3ai.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | nne 3020 | . . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
3 | 1, 2 | sylibr 235 | . 2 ⊢ (𝜑 → ¬ 𝐴 ≠ 𝐵) |
4 | 3 | con2i 141 | 1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1528 ≠ wne 3016 |
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 208 df-ne 3017 |
This theorem is referenced by: necon1ai 3043 necon3i 3048 neneor 3118 nelsn 4597 disjsn2 4642 prnesn 4784 opelopabsb 5409 funsndifnop 6906 map0b 8437 mapdom3 8678 cflim2 9674 isfin4p1 9726 fpwwe2lem13 10053 tskuni 10194 recextlem2 11260 hashprg 13746 eqsqrt2d 14718 gcd1 15866 gcdzeq 15892 lcmfunsnlem2lem1 15972 lcmfunsnlem2lem2 15973 phimullem 16106 pcgcd1 16203 pc2dvds 16205 pockthlem 16231 ablfacrplem 19118 znrrg 20642 opnfbas 22380 supfil 22433 itg1addlem4 24229 itg1addlem5 24230 dvdsmulf1o 25699 ppiub 25708 dchrelbas4 25747 2sqlem8 25930 tgldimor 26216 subfacp1lem6 32330 cvmsss2 32419 ax6e2ndeq 40773 supminfxr2 41625 fourierdlem56 42328 ichnreuop 43481 |
Copyright terms: Public domain | W3C validator |