![]() |
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 139 | . 2 ⊢ (𝜓 → ¬ ¬ 𝜓) | |
2 | necon4ad.1 | . . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) | |
3 | 2 | necon1bd 2989 | . 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 = 𝐵)) |
4 | 1, 3 | syl5 34 | 1 ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1653 ≠ wne 2971 |
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 199 df-ne 2972 |
This theorem is referenced by: necon1d 2993 fisseneq 8413 f1finf1o 8429 dfac5 9237 isf32lem9 9471 fpwwe2 9753 qextlt 12283 qextle 12284 xsubge0 12340 hashf1 13490 climuni 14624 rpnnen2lem12 15290 fzo0dvdseq 15384 4sqlem11 15992 haust1 21485 deg1lt0 24192 ply1divmo 24236 ig1peu 24272 dgrlt 24363 quotcan 24405 fta 25158 atcv0eq 29763 erdszelem9 31698 poimirlem23 33921 poimir 33931 lshpdisj 35008 lsatcv0eq 35068 exatleN 35425 atcvr0eq 35447 cdlemg31c 36720 jm2.19 38345 jm2.26lem3 38353 dgraa0p 38504 |
Copyright terms: Public domain | W3C validator |