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 3444 difundi 3461 dcun 3606 sotricim 4426 sotritrieq 4428 en2lp 4658 poxp 6406 nntri2 6705 finexdc 7135 elssdc 7137 unfidisj 7157 fidcenumlemrks 7195 pw1nel3 7509 sucpw1nel3 7511 onntri45 7519 aptipr 7921 lttri3 8318 letr 8321 apirr 8844 apti 8861 elnnz 9550 xrlttri3 10093 xrletr 10104 exp3val 10866 bcval4 11077 hashunlem 11130 maxleast 11853 xrmaxlesup 11899 lcmval 12715 lcmcllem 12719 lcmgcdlem 12729 isprm3 12770 pcpremul 12946 ivthinc 15454 lgsdir2 15852 2lgslem3 15920 structiedg0val 15981 vtxd0nedgbfi 16240 vdegp1aid 16255 bj-nnor 16452 pwtrufal 16719 pwle2 16720

W3C validator