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 771, anordc 945, or ianordc 889. 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 728 | . . 3 | |
2 | pm2.46 729 | . . 3 | |
3 | 1, 2 | jca 304 | . 2 |
4 | simpl 108 | . . . . 5 | |
5 | 4 | con2i 617 | . . . 4 |
6 | simpr 109 | . . . . 5 | |
7 | 6 | con2i 617 | . . . 4 |
8 | 5, 7 | jaoi 706 | . . 3 |
9 | 8 | con2i 617 | . 2 |
10 | 3, 9 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wa 103 wb 104 wo 698 |
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 604 ax-in2 605 ax-io 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm4.56 770 nnexmid 840 dcor 924 3ioran 982 3ori 1289 unssdif 3352 difundi 3369 dcun 3514 sotricim 4295 sotritrieq 4297 en2lp 4525 poxp 6191 nntri2 6453 finexdc 6859 unfidisj 6878 fidcenumlemrks 6909 pw1nel3 7178 sucpw1nel3 7180 onntri45 7188 aptipr 7573 lttri3 7969 letr 7972 apirr 8494 apti 8511 elnnz 9192 xrlttri3 9724 xrletr 9735 exp3val 10447 bcval4 10654 hashunlem 10706 maxleast 11141 xrmaxlesup 11186 lcmval 11974 lcmcllem 11978 lcmgcdlem 11988 isprm3 12029 pcpremul 12204 ivthinc 13168 bj-nnor 13458 pwtrufal 13718 pwle2 13719 |
Copyright terms: Public domain | W3C validator |