Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > necon3abii | Structured version Visualization version Unicode version |
Description: Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.) |
Ref | Expression |
---|---|
necon3abii.1 |
Ref | Expression |
---|---|
necon3abii |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2795 | . 2 | |
2 | necon3abii.1 | . 2 | |
3 | 1, 2 | xchbinx 324 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wb 196 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-ne 2795 |
This theorem is referenced by: necon3bbii 2841 necon3bii 2846 nesym 2850 n0fOLD 3928 rabn0 3958 xpimasn 5579 rankxplim3 8744 rankxpsuc 8745 dflt2 11981 gcd0id 15240 lcmfunsnlem2 15353 axlowdimlem13 25834 filnetlem4 32376 dihatlat 36623 pellex 37399 nev 38062 ldepspr 42262 |
Copyright terms: Public domain | W3C validator |