![]() |
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 142 | . 2 ⊢ (𝜓 → ¬ ¬ 𝜓) | |
2 | necon4ad.1 | . . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) | |
3 | 2 | necon1bd 2947 | . 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 = 𝐵)) |
4 | 1, 3 | syl5 34 | 1 ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1533 ≠ wne 2929 |
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 2930 |
This theorem is referenced by: necon1d 2951 fisseneq 9282 f1finf1o 9296 f1finf1oOLD 9297 dfac5 10153 isf32lem9 10386 fpwwe2 10668 qextlt 13217 qextle 13218 xsubge0 13275 hashf1 14454 climuni 15532 rpnnen2lem12 16205 fzo0dvdseq 16303 4sqlem11 16927 haust1 23300 deg1lt0 26071 ply1divmo 26116 ig1peu 26154 dgrlt 26246 quotcan 26289 fta 27057 atcv0eq 32261 erdszelem9 34937 poimirlem23 37244 poimir 37254 lshpdisj 38586 lsatcv0eq 38646 exatleN 39004 atcvr0eq 39026 cdlemg31c 40299 itrere 42011 sn-itrere 42153 sn-retire 42154 jm2.19 42553 jm2.26lem3 42561 dgraa0p 42712 |
Copyright terms: Public domain | W3C validator |