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 3029 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ ¬ 𝜓)) |
3 | notnotr 132 | . 2 ⊢ (¬ ¬ 𝜓 → 𝜓) | |
4 | 2, 3 | syl6 35 | 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: prnebg 4780 fr0 5528 sofld 6038 onmindif2 7515 suppss 7851 suppss2 7855 uniinqs 8367 dfac5lem4 9541 uzwo 12300 seqf1olem1 13399 seqf1olem2 13400 hashnncl 13717 pceq0 16197 vdwmc2 16305 odcau 18660 islss 19637 fidomndrnglem 20009 mvrf1 20135 mpfrcl 20228 obs2ss 20803 obslbs 20804 dsmmacl 20815 regr1lem2 22278 iccpnfhmeo 23478 itg10a 24240 dvlip 24519 deg1ge 24621 elply2 24715 coeeulem 24743 dgrle 24762 coemullem 24769 basellem2 25587 perfectlem2 25734 lgsabs1 25840 lnon0 28503 atsseq 30052 disjif2 30260 cvmseu 32421 nosepon 33070 noextenddif 33073 matunitlindf 34772 poimirlem2 34776 poimirlem18 34792 poimirlem21 34795 itg2addnclem 34825 lsatcmp 36021 lsatcmp2 36022 ltrnnid 37154 trlatn0 37190 cdlemh 37835 dochlkr 38403 perfectALTVlem2 43734 |
Copyright terms: Public domain | W3C validator |