Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > necon4ad | Structured version Visualization version GIF version |
Description: Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
Ref | Expression |
---|---|
necon4ad.1 | ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) |
Ref | Expression |
---|---|
necon4ad | ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnot 144 | . 2 ⊢ (𝜓 → ¬ ¬ 𝜓) | |
2 | necon4ad.1 | . . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) | |
3 | 2 | necon1bd 3032 | . 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 = 𝐵)) |
4 | 1, 3 | syl5 34 | 1 ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1531 ≠ wne 3014 |
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 209 df-ne 3015 |
This theorem is referenced by: necon1d 3036 fisseneq 8721 f1finf1o 8737 dfac5 9546 isf32lem9 9775 fpwwe2 10057 qextlt 12588 qextle 12589 xsubge0 12646 hashf1 13807 climuni 14901 rpnnen2lem12 15570 fzo0dvdseq 15665 4sqlem11 16283 haust1 21952 deg1lt0 24677 ply1divmo 24721 ig1peu 24757 dgrlt 24848 quotcan 24890 fta 25649 atcv0eq 30148 erdszelem9 32439 poimirlem23 34907 poimir 34917 lshpdisj 36115 lsatcv0eq 36175 exatleN 36532 atcvr0eq 36554 cdlemg31c 37827 jm2.19 39581 jm2.26lem3 39589 dgraa0p 39740 |
Copyright terms: Public domain | W3C validator |