ne3anior - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ne3anior		Structured version Visualization version Unicode version

Theorem ne3anior 2887

Description: A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.)

**Assertion**
Ref	Expression
ne3anior	$/\$ $/\$ $\/$ $\/$

**Proof of Theorem ne3anior**
Step	Hyp	Ref	Expression
1		3anor 1054	. 2 $/\$ $/\$ $\/$ $\/$
2		nne 2798	. . 3
3		nne 2798	. . 3
4		nne 2798	. . 3
5	2, 3, 4	3orbi123i 1252	. 2 $\/$ $\/$ $\/$ $\/$
6	1, 5	xchbinx 324	1 $/\$ $/\$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 196 $\/$ w3o 1036 $/\$ w3a 1037

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-3or 1038 df-3an 1039 df-ne 2795

This theorem is referenced by: eldiftp 4228