Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ioran | Unicode version |
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 770, anordc 940, or ianordc 884. Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Ref | Expression |
---|---|
ioran |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.45 727 | . . 3 | |
2 | pm2.46 728 | . . 3 | |
3 | 1, 2 | jca 304 | . 2 |
4 | simpl 108 | . . . . 5 | |
5 | 4 | con2i 616 | . . . 4 |
6 | simpr 109 | . . . . 5 | |
7 | 6 | con2i 616 | . . . 4 |
8 | 5, 7 | jaoi 705 | . . 3 |
9 | 8 | con2i 616 | . 2 |
10 | 3, 9 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wa 103 wb 104 wo 697 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 603 ax-in2 604 ax-io 698 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm4.56 769 nnexmid 835 dcor 919 3ioran 977 3ori 1278 unssdif 3311 difundi 3328 dcun 3473 sotricim 4245 sotritrieq 4247 en2lp 4469 poxp 6129 nntri2 6390 finexdc 6796 unfidisj 6810 fidcenumlemrks 6841 aptipr 7449 lttri3 7844 letr 7847 apirr 8367 apti 8384 elnnz 9064 xrlttri3 9583 xrletr 9591 exp3val 10295 bcval4 10498 hashunlem 10550 maxleast 10985 xrmaxlesup 11028 lcmval 11744 lcmcllem 11748 lcmgcdlem 11758 isprm3 11799 ivthinc 12790 bj-nnor 12946 pwtrufal 13192 pwle2 13193 |
Copyright terms: Public domain | W3C validator |