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 7590 sucpw1nel3 7592 onntri45 7600 aptipr 8008 lttri3 8405 letr 8408 apirr 8935 apti 8952 elnnz 9658 xrlttri3 10209 xrletr 10220 exp3val 10991 bcval4 11204 hashunlem 11258 maxleast 11994 xrmaxlesup 12041 lcmval 12857 lcmcllem 12861 lcmgcdlem 12871 isprm3 12912 pcpremul 13092 ivthinc 15793 lgsdir2 16250 2lgslem3 16318 structiedg0val 16379 vtxd0nedgbfi 16638 vdegp1aid 16653 bj-nnor 16860 pwtrufal 17125 pwle2 17126

W3C validator