![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ioran | GIF 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 941, or ianordc 885. 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 836 dcor 920 3ioran 978 3ori 1279 unssdif 3316 difundi 3333 dcun 3478 sotricim 4253 sotritrieq 4255 en2lp 4477 poxp 6137 nntri2 6398 finexdc 6804 unfidisj 6818 fidcenumlemrks 6849 aptipr 7473 lttri3 7868 letr 7871 apirr 8391 apti 8408 elnnz 9088 xrlttri3 9613 xrletr 9621 exp3val 10326 bcval4 10530 hashunlem 10582 maxleast 11017 xrmaxlesup 11060 lcmval 11780 lcmcllem 11784 lcmgcdlem 11794 isprm3 11835 ivthinc 12829 bj-nnor 13117 pwtrufal 13365 pwle2 13366 |
Copyright terms: Public domain | W3C validator |