ioran - Intuitionistic Logic Explorer

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

Theorem ioran 757

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 786, anordc 962, or ianordc 904. 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 743	. . 3 $\/$
2		pm2.46 744	. . 3 $\/$
3	1, 2	jca 306	. 2 $\/$ $/\$
4		simpl 109	. . . . 5 $/\$
5	4	con2i 630	. . . 4 $/\$
6		simpr 110	. . . . 5 $/\$
7	6	con2i 630	. . . 4 $/\$
8	5, 7	jaoi 721	. . 3 $\/$ $/\$
9	8	con2i 630	. 2 $/\$ $\/$
10	3, 9	impbii 126	1 $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3 $/\$ wa 104

wb 105 $\/$ wo 713

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 617 ax-in2 618 ax-io 714

This theorem depends on definitions: df-bi 117

This theorem is referenced by: pm4.56 785 nnexmid 855 dcor 941 3ioran 1017 3ori 1334 ecase2d 1385 unssdif 3439 difundi 3456 dcun 3601 sotricim 4414 sotritrieq 4416 en2lp 4646 poxp 6384 nntri2 6648 finexdc 7073 elssdc 7075 unfidisj 7095 fidcenumlemrks 7131 pw1nel3 7427 sucpw1nel3 7429 onntri45 7437 aptipr 7839 lttri3 8237 letr 8240 apirr 8763 apti 8780 elnnz 9467 xrlttri3 10005 xrletr 10016 exp3val 10775 bcval4 10986 hashunlem 11038 maxleast 11740 xrmaxlesup 11786 lcmval 12601 lcmcllem 12605 lcmgcdlem 12615 isprm3 12656 pcpremul 12832 ivthinc 15333 lgsdir2 15728 2lgslem3 15796 structiedg0val 15857 vtxd0nedgbfi 16059 bj-nnor 16181 pwtrufal 16450 pwle2 16451

W3C validator