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 2947 | . 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ ¬ 𝜓)) |
3 | notnotr 132 | . 2 ⊢ (¬ ¬ 𝜓 → 𝜓) | |
4 | 2, 3 | syl6 35 | 1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1542 ≠ wne 2934 |
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 210 df-ne 2935 |
This theorem is referenced by: prnebg 4741 fr0 5504 sofld 6019 onmindif2 7546 suppss 7889 suppssOLD 7890 suppss2 7895 uniinqs 8408 dfac5lem4 9626 uzwo 12393 seqf1olem1 13501 seqf1olem2 13502 hashnncl 13819 pceq0 16307 vdwmc2 16415 odcau 18847 islss 19825 fidomndrnglem 20198 obs2ss 20545 obslbs 20546 dsmmacl 20557 mvrf1 20804 mpfrcl 20899 mhpvarcl 20942 regr1lem2 22491 iccpnfhmeo 23697 itg10a 24463 dvlip 24745 deg1ge 24851 elply2 24945 coeeulem 24973 dgrle 24992 coemullem 24999 basellem2 25819 perfectlem2 25966 lgsabs1 26072 lnon0 28733 atsseq 30282 disjif2 30494 prmidl0 31198 cvmseu 32809 nosepon 33509 noextenddif 33512 matunitlindf 35398 poimirlem2 35402 poimirlem18 35418 poimirlem21 35421 itg2addnclem 35451 lsatcmp 36640 lsatcmp2 36641 ltrnnid 37773 trlatn0 37809 cdlemh 38454 dochlkr 39022 perfectALTVlem2 44708 |
Copyright terms: Public domain | W3C validator |