Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > neeq12d | Structured version Visualization version Unicode version |
Description: Deduction for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
Ref | Expression |
---|---|
neeq1d.1 | |
neeq12d.2 |
Ref | Expression |
---|---|
neeq12d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neeq1d.1 | . . 3 | |
2 | neeq12d.2 | . . 3 | |
3 | 1, 2 | eqeq12d 2637 | . 2 |
4 | 3 | necon3bid 2838 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wceq 1483 wne 2794 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 df-ne 2795 |
This theorem is referenced by: fnelnfp 6443 suppval 7297 infpssrlem4 9128 injresinjlem 12588 sgrp2nmndlem5 17416 pmtr3ncom 17895 isnzr 19259 ptcmplem2 21857 isinag 25729 axlowdimlem6 25827 axlowdimlem14 25835 pthdadjvtx 26626 uhgrwkspthlem2 26650 usgr2wlkspth 26655 usgr2trlncl 26656 pthdlem1 26662 lfgrn1cycl 26697 2wlkdlem5 26825 2pthdlem1 26826 3wlkdlem5 27023 3pthdlem1 27024 numclwwlk2lem1 27235 numclwlk2lem2f 27236 numclwlk2lem2f1o 27238 eulplig 27337 signsvvfval 30655 signsvfn 30659 bnj1534 30923 bnj1542 30927 bnj1280 31088 derangsn 31152 derangenlem 31153 subfacp1lem3 31164 subfacp1lem5 31166 subfacp1lem6 31167 subfacp1 31168 sltval2 31809 sltres 31815 noseponlem 31817 noextenddif 31821 nosepnelem 31830 nosepeq 31835 nosupbnd2lem1 31861 noetalem3 31865 fvtransport 32139 poimirlem1 33410 poimirlem6 33415 poimirlem7 33416 cdlemkid3N 36221 cdlemkid4 36222 stoweidlem43 40260 nnsgrpnmnd 41818 2zrngnmlid 41949 pgrpgt2nabl 42147 ldepsnlinc 42297 |
Copyright terms: Public domain | W3C validator |