Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > necon3ad | Structured version Visualization version GIF version |
Description: Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
Ref | Expression |
---|---|
necon3ad.1 | ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) |
Ref | Expression |
---|---|
necon3ad | ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3ad.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) | |
2 | neneq 3022 | . 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵) | |
3 | 1, 2 | nsyli 160 | 1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1533 ≠ 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 209 df-ne 3017 |
This theorem is referenced by: necon1ad 3033 necon3d 3037 disjpss 4409 2f1fvneq 7017 oeeulem 8226 enp1i 8752 canthp1lem2 10074 winalim2 10117 nlt1pi 10327 sqreulem 14718 rpnnen2lem11 15576 eucalglt 15928 nprm 16031 pcprmpw2 16217 pcmpt 16227 expnprm 16237 prmlem0 16438 pltnle 17575 psgnunilem1 18620 pgpfi 18729 frgpnabllem1 18992 gsumval3a 19022 ablfac1eulem 19193 pgpfaclem2 19203 ablsimpgfindlem1 19228 lspdisjb 19897 lspdisj2 19898 obselocv 20871 0nnei 21719 t0dist 21932 t1sep 21977 ordthauslem 21990 hausflim 22588 bcthlem5 23930 bcth 23931 fta1g 24760 plyco0 24781 dgrnznn 24836 coeaddlem 24838 fta1 24896 vieta1lem2 24899 logcnlem3 25226 dvloglem 25230 dcubic 25423 mumullem2 25756 2sqlem8a 26000 dchrisum0flblem1 26083 colperpexlem2 26516 elntg2 26770 1loopgrnb0 27283 usgr2trlncrct 27583 ocnel 29074 hatomistici 30138 lbslsat 31014 sibfof 31598 outsideofrflx 33588 poimirlem23 34914 mblfinlem1 34928 cntotbnd 35073 heiborlem6 35093 lshpnel 36118 lshpcmp 36123 lfl1 36205 lkrshp 36240 lkrpssN 36298 atnlt 36448 atnle 36452 atlatmstc 36454 intnatN 36542 atbtwn 36581 llnnlt 36658 lplnnlt 36700 2llnjaN 36701 lvolnltN 36753 2lplnja 36754 dalem-cly 36806 dalem44 36851 2llnma3r 36923 cdlemblem 36928 lhpm0atN 37164 lhp2atnle 37168 cdlemednpq 37434 cdleme22cN 37477 cdlemg18b 37814 cdlemg42 37864 dia2dimlem1 38199 dochkrshp 38521 hgmapval0 39027 rrx2pnecoorneor 44701 |
Copyright terms: Public domain | W3C validator |