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 6772 finexdc 7213 elssdc 7215 unfidisj 7235 fidcenumlemrks 7277 pw1nel3 7596 sucpw1nel3 7598 onntri45 7606 aptipr 8014 lttri3 8411 letr 8414 apirr 8941 apti 8958 elnnz 9663 xrlttri3 10215 xrletr 10226 exp3val 10998 bcval4 11211 hashunlem 11265 maxleast 12001 xrmaxlesup 12049 lcmval 12865 lcmcllem 12869 lcmgcdlem 12879 isprm3 12920 pcpremul 13100 ivthinc 15886 lgsdir2 16374 2lgslem3 16442 structiedg0val 16503 vtxd0nedgbfi 16762 vdegp1aid 16777 bj-nnor 16984 pwtrufal 17249 pwle2 17250

W3C validator