![]() |
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 2945 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ ¬ 𝜓)) |
3 | notnotr 125 | . 2 ⊢ (¬ ¬ 𝜓 → 𝜓) | |
4 | 2, 3 | syl6 35 | 1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1632 ≠ wne 2932 |
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 197 df-ne 2933 |
This theorem is referenced by: prnebg 4533 fr0 5245 sofld 5739 onmindif2 7178 suppss 7495 suppss2 7499 uniinqs 7996 dfac5lem4 9159 uzwo 11964 seqf1olem1 13054 seqf1olem2 13055 hashnncl 13369 pceq0 15797 vdwmc2 15905 odcau 18239 islss 19157 fidomndrnglem 19528 mvrf1 19647 mpfrcl 19740 obs2ss 20295 obslbs 20296 dsmmacl 20307 regr1lem2 21765 iccpnfhmeo 22965 itg10a 23696 dvlip 23975 deg1ge 24077 elply2 24171 coeeulem 24199 dgrle 24218 coemullem 24225 basellem2 25028 perfectlem2 25175 lgsabs1 25281 lnon0 27983 atsseq 29536 disjif2 29722 cvmseu 31586 nosepon 32145 noextenddif 32148 matunitlindf 33738 poimirlem2 33742 poimirlem18 33758 poimirlem21 33761 itg2addnclem 33792 lsatcmp 34811 lsatcmp2 34812 ltrnnid 35943 trlatn0 35980 cdlemh 36625 dochlkr 37194 perfectALTVlem2 42159 |
Copyright terms: Public domain | W3C validator |