ioran - Intuitionistic Logic Explorer

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

Theorem ioran 760

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 789, anordc 965, or ianordc 907. 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 746	. . 3 $\/$
2		pm2.46 747	. . 3 $\/$
3	1, 2	jca 306	. 2 $\/$ $/\$
4		simpl 109	. . . . 5 $/\$
5	4	con2i 632	. . . 4 $/\$
6		simpr 110	. . . . 5 $/\$
7	6	con2i 632	. . . 4 $/\$
8	5, 7	jaoi 724	. . 3 $\/$ $/\$
9	8	con2i 632	. 2 $/\$ $\/$
10	3, 9	impbii 126	1 $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3 $/\$ wa 104

wb 105 $\/$ wo 716

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 619 ax-in2 620 ax-io 717

This theorem depends on definitions: df-bi 117

This theorem is referenced by: pm4.56 788 nnexmid 858 dcor 944 3ioran 1020 3ori 1337 ecase2d 1388 unssdif 3458 difundi 3475 dcun 3621 sotricim 4446 sotritrieq 4448 en2lp 4678 poxp 6430 nntri2 6729 finexdc 7162 elssdc 7164 unfidisj 7184 fidcenumlemrks 7225 pw1nel3 7543 sucpw1nel3 7545 onntri45 7553 aptipr 7958 lttri3 8355 letr 8358 apirr 8881 apti 8898 elnnz 9589 xrlttri3 10133 xrletr 10144 exp3val 10907 bcval4 11118 hashunlem 11172 maxleast 11902 xrmaxlesup 11948 lcmval 12764 lcmcllem 12768 lcmgcdlem 12778 isprm3 12819 pcpremul 12995 ivthinc 15525 lgsdir2 15923 2lgslem3 15991 structiedg0val 16052 vtxd0nedgbfi 16311 vdegp1aid 16326 bj-nnor 16523 pwtrufal 16788 pwle2 16789

W3C validator