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 3026 | . 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 3013 |
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 3014 |
This theorem is referenced by: prnebg 4778 fr0 5527 sofld 6037 onmindif2 7516 suppss 7849 suppss2 7853 uniinqs 8366 dfac5lem4 9540 uzwo 12299 seqf1olem1 13397 seqf1olem2 13398 hashnncl 13715 pceq0 16195 vdwmc2 16303 odcau 18658 islss 19635 fidomndrnglem 20007 mvrf1 20133 mpfrcl 20226 obs2ss 20801 obslbs 20802 dsmmacl 20813 regr1lem2 22276 iccpnfhmeo 23476 itg10a 24238 dvlip 24517 deg1ge 24619 elply2 24713 coeeulem 24741 dgrle 24760 coemullem 24767 basellem2 25586 perfectlem2 25733 lgsabs1 25839 lnon0 28502 atsseq 30051 disjif2 30259 cvmseu 32420 nosepon 33069 noextenddif 33072 matunitlindf 34771 poimirlem2 34775 poimirlem18 34791 poimirlem21 34794 itg2addnclem 34824 lsatcmp 36019 lsatcmp2 36020 ltrnnid 37152 trlatn0 37188 cdlemh 37833 dochlkr 38401 perfectALTVlem2 43764 |
Copyright terms: Public domain | W3C validator |