Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > neanior | Structured version Visualization version Unicode version |
Description: A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.) |
Ref | Expression |
---|---|
neanior |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2795 | . . 3 | |
2 | df-ne 2795 | . . 3 | |
3 | 1, 2 | anbi12i 733 | . 2 |
4 | pm4.56 516 | . 2 | |
5 | 3, 4 | bitri 264 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wb 196 wo 383 wa 384 wceq 1483 wne 2794 |
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-or 385 df-an 386 df-ne 2795 |
This theorem is referenced by: nelpri 4201 nelprd 4203 eldifpr 4204 0nelop 4960 om00 7655 om00el 7656 oeoe 7679 mulne0b 10668 xmulpnf1 12104 lcmgcd 15320 lcmdvds 15321 drngmulne0 18769 lvecvsn0 19109 domnmuln0 19298 abvn0b 19302 mdetralt 20414 ply1domn 23883 vieta1lem1 24065 vieta1lem2 24066 atandm 24603 atandm3 24605 dchrelbas3 24963 eupth2lem3lem7 27094 frgrreg 27252 nmlno0lem 27648 nmlnop0iALT 28854 chirredi 29253 subfacp1lem1 31161 filnetlem4 32376 lcvbr3 34310 cvrnbtwn4 34566 elpadd0 35095 cdleme0moN 35512 cdleme0nex 35577 isdomn3 37782 lidldomnnring 41930 |
Copyright terms: Public domain | W3C validator |