![]() |
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 846, anordc 903, or ianordc 838. 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 693 | . . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑) | |
2 | pm2.46 694 | . . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓) | |
3 | 1, 2 | jca 301 | . 2 ⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∧ ¬ 𝜓)) |
4 | simpl 108 | . . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑) | |
5 | 4 | con2i 593 | . . . 4 ⊢ (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓)) |
6 | simpr 109 | . . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓) | |
7 | 6 | con2i 593 | . . . 4 ⊢ (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓)) |
8 | 5, 7 | jaoi 672 | . . 3 ⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓)) |
9 | 8 | con2i 593 | . 2 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓)) |
10 | 3, 9 | impbii 125 | 1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∧ wa 103 ↔ wb 104 ∨ wo 665 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 580 ax-in2 581 ax-io 666 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm4.56 845 dcor 882 3ioran 940 3ori 1237 unssdif 3237 difundi 3254 dcun 3398 sotricim 4161 sotritrieq 4163 en2lp 4385 poxp 6013 nntri2 6271 finexdc 6674 unfidisj 6688 fidcenumlemrks 6718 aptipr 7263 lttri3 7628 letr 7631 apirr 8145 apti 8162 elnnz 8823 xrlttri3 9330 xrletr 9336 exp3val 10020 bcval4 10223 hashunlem 10275 maxleast 10709 lcmval 11386 lcmcllem 11390 lcmgcdlem 11400 isprm3 11441 nnexmid 11964 |
Copyright terms: Public domain | W3C validator |