ianor - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem ianor 305

Description: Negated conjunction in terms of disjunction (DeMorgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120.

**Assertion**
Ref	Expression
ianor	$/\$ $\/$

**Proof of Theorem ianor**
Step	Hyp	Ref	Expression
1		anor 304	. . 3 $/\$ $\/$
2	1	negbii 187	. 2 $/\$ $\/$
3		pm4.13 161	. 2 $\/$ $\/$
4	2, 3	bitr4 176	1 $/\$ $\/$

Colors of variables: wff set class

Syntax hints:

wn 2

wb 146 $\/$ wo 222 $/\$ wa 223

This theorem is referenced by: pm4.79 355 andi 602 pm3.24 656 pm5.18 658 pm5.16 665 19.33b 1088 19.41 1091 neorian 1632 pssn2lp 2137 ordtri3or 2969 suc11 3083 xpeq0 3453 imadif 3560 mapdom2 4474 suc11reg 4577 rankxplim3 4686 kmlem3 4739 ssgt0sr 5189 xrrebndt 5541 bcval4t 6899 efif1lem5 8649 chrelat2 10200 atcvat 10221 cdrci 10381

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225