| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > necon1ad | Structured version Visualization version GIF version | ||
| Description: Contrapositive deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
| Ref | Expression |
|---|---|
| necon1ad.1 | ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵)) |
| Ref | Expression |
|---|---|
| necon1ad | ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | necon1ad.1 | . . 3 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵)) | |
| 2 | 1 | necon3ad 2953 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ ¬ 𝜓)) |
| 3 | notnotr 130 | . 2 ⊢ (¬ ¬ 𝜓 → 𝜓) | |
| 4 | 2, 3 | syl6 35 | 1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1540 ≠ wne 2940 |
| 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 207 df-ne 2941 |
| This theorem is referenced by: prnebg 4856 fr0 5663 sofld 6207 onmindif2 7827 suppss 8219 suppss2 8225 uniinqs 8837 dfac5lem4 10166 dfac5lem4OLD 10168 uzwo 12953 seqf1olem1 14082 seqf1olem2 14083 hashnncl 14405 pceq0 16909 vdwmc2 17017 odcau 19622 fidomndrnglem 20773 islss 20932 obs2ss 21749 obslbs 21750 dsmmacl 21761 mvrf1 22006 mpfrcl 22109 mhpvarcl 22152 regr1lem2 23748 iccpnfhmeo 24976 itg10a 25745 dvlip 26032 deg1ge 26137 elply2 26235 coeeulem 26263 dgrle 26282 coemullem 26289 basellem2 27125 perfectlem2 27274 lgsabs1 27380 nosepon 27710 noextenddif 27713 lnon0 30817 atsseq 32366 disjif2 32594 prmidl0 33478 cvmseu 35281 matunitlindf 37625 poimirlem2 37629 poimirlem18 37645 poimirlem21 37648 itg2addnclem 37678 lsatcmp 39004 lsatcmp2 39005 ltrnnid 40138 trlatn0 40174 cdlemh 40819 dochlkr 41387 perfectALTVlem2 47709 |
| Copyright terms: Public domain | W3C validator |