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 3034 | . 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 = 𝐵)) |
4 | 1, 3 | syl5 34 | 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: necon1d 3038 fisseneq 8718 f1finf1o 8734 dfac5 9543 isf32lem9 9772 fpwwe2 10054 qextlt 12586 qextle 12587 xsubge0 12644 hashf1 13805 climuni 14899 rpnnen2lem12 15568 fzo0dvdseq 15663 4sqlem11 16281 haust1 21890 deg1lt0 24614 ply1divmo 24658 ig1peu 24694 dgrlt 24785 quotcan 24827 fta 25585 atcv0eq 30084 erdszelem9 32344 poimirlem23 34797 poimir 34807 lshpdisj 36005 lsatcv0eq 36065 exatleN 36422 atcvr0eq 36444 cdlemg31c 37717 jm2.19 39470 jm2.26lem3 39478 dgraa0p 39629 |
Copyright terms: Public domain | W3C validator |