neorian - Metamath Proof Explorer

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

Theorem neorian 2888

Description: A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)

**Assertion**
Ref	Expression
neorian	$\/$ $/\$

**Proof of Theorem neorian**
Step	Hyp	Ref	Expression
1		df-ne 2795	. . 3
2		df-ne 2795	. . 3
3	1, 2	orbi12i 543	. 2 $\/$ $\/$
4		ianor 509	. 2 $/\$ $\/$
5	3, 4	bitr4i 267	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: neneor 2893 oeoa 7677 wemapso2lem 8457 recextlem2 10658 crne0 11013 crreczi 12989 gcdcllem3 15223 bezoutlem2 15257 dsmmacl 20085 txhaus 21450 itg1addlem2 23464 coeaddlem 24005 dcubic 24573 sibfof 30402 nrhmzr 41873