ioran - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > ioran		Unicode version

Theorem ioran 764

Description: Negated disjunction in terms of conjunction. This version of DeMorgan's law is a biconditional for all propositions (not just decidable ones), unlike oranim 793, anordc 969, or ianordc 911. Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)

**Assertion**
Ref	Expression
ioran	$\/$ $/\$

**Proof of Theorem ioran**
Step	Hyp	Ref	Expression
1		pm2.45 750	. . 3 $\/$
2		pm2.46 751	. . 3 $\/$
3	1, 2	jca 306	. 2 $\/$ $/\$
4		simpl 109	. . . . 5 $/\$
5	4	con2i 636	. . . 4 $/\$
6		simpr 110	. . . . 5 $/\$
7	6	con2i 636	. . . 4 $/\$
8	5, 7	jaoi 728	. . 3 $\/$ $/\$
9	8	con2i 636	. 2 $/\$ $\/$
10	3, 9	impbii 126	1 $\/$ $/\$

Colors of variables: wff set class

This proof depends on syntax axioms:

wn 3 $/\$ wa 104

wb 105 $\/$ wo 720

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721

This proof depends on definitions: df-bi 117

This theorem is used by: pm4.56 792 nnexmid 862 dcor 948 3ioran 1024 3ori 1341 ecase2d 1392 unssdif 3466 difundi 3483 dcun 3637 sotricim 4470 sotritrieq 4472 en2lp 4703 poxp 6472 nntri2 6771 finexdc 7211 elssdc 7213 unfidisj 7233 fidcenumlemrks 7275 pw1nel3 7596 sucpw1nel3 7598 onntri45 7606 aptipr 8014 lttri3 8411 letr 8414 apirr 8941 apti 8958 elnnz 9665 xrlttri3 10216 xrletr 10227 exp3val 10999 bcval4 11212 hashunlem 11266 maxleast 12002 xrmaxlesup 12050 lcmval 12866 lcmcllem 12870 lcmgcdlem 12880 isprm3 12921 pcpremul 13101 ivthinc 15869 lgsdir2 16357 2lgslem3 16425 structiedg0val 16486 vtxd0nedgbfi 16745 vdegp1aid 16760 bj-nnor 16967 pwtrufal 17232 pwle2 17233

W3C validator