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 4468 sotritrieq 4470 en2lp 4701 poxp 6468 nntri2 6767 finexdc 7207 elssdc 7209 unfidisj 7229 fidcenumlemrks 7270 pw1nel3 7591 sucpw1nel3 7593 onntri45 7601 aptipr 8009 lttri3 8406 letr 8409 apirr 8936 apti 8953 elnnz 9659 xrlttri3 10210 xrletr 10221 exp3val 10993 bcval4 11206 hashunlem 11260 maxleast 11996 xrmaxlesup 12044 lcmval 12860 lcmcllem 12864 lcmgcdlem 12874 isprm3 12915 pcpremul 13095 ivthinc 15835 lgsdir2 16318 2lgslem3 16386 structiedg0val 16447 vtxd0nedgbfi 16706 vdegp1aid 16721 bj-nnor 16928 pwtrufal 17193 pwle2 17194

W3C validator