![]() |
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 1542 ≠ 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 206 df-ne 2941 |
This theorem is referenced by: prnebg 4817 fr0 5616 sofld 6143 onmindif2 7746 suppss 8129 suppssOLD 8130 suppss2 8135 uniinqs 8742 dfac5lem4 10070 uzwo 12844 seqf1olem1 13956 seqf1olem2 13957 hashnncl 14275 pceq0 16751 vdwmc2 16859 odcau 19394 islss 20439 fidomndrnglem 20800 obs2ss 21158 obslbs 21159 dsmmacl 21170 mvrf1 21417 mpfrcl 21518 mhpvarcl 21561 regr1lem2 23114 iccpnfhmeo 24331 itg10a 25098 dvlip 25380 deg1ge 25486 elply2 25580 coeeulem 25608 dgrle 25627 coemullem 25634 basellem2 26454 perfectlem2 26601 lgsabs1 26707 nosepon 27036 noextenddif 27039 lnon0 29789 atsseq 31338 disjif2 31552 prmidl0 32278 cvmseu 33934 matunitlindf 36126 poimirlem2 36130 poimirlem18 36146 poimirlem21 36149 itg2addnclem 36179 lsatcmp 37515 lsatcmp2 37516 ltrnnid 38649 trlatn0 38685 cdlemh 39330 dochlkr 39898 perfectALTVlem2 46004 |
Copyright terms: Public domain | W3C validator |