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 3460 difundi 3477 dcun 3623 sotricim 4449 sotritrieq 4451 en2lp 4681 poxp 6441 nntri2 6740 finexdc 7173 elssdc 7175 unfidisj 7195 fidcenumlemrks 7236 pw1nel3 7554 sucpw1nel3 7556 onntri45 7564 aptipr 7972 lttri3 8369 letr 8372 apirr 8896 apti 8913 elnnz 9604 xrlttri3 10149 xrletr 10160 exp3val 10927 bcval4 11139 hashunlem 11193 maxleast 11923 xrmaxlesup 11969 lcmval 12785 lcmcllem 12789 lcmgcdlem 12799 isprm3 12840 pcpremul 13016 ivthinc 15634 lgsdir2 16032 2lgslem3 16100 structiedg0val 16161 vtxd0nedgbfi 16420 vdegp1aid 16435 bj-nnor 16632 pwtrufal 16897 pwle2 16898

W3C validator