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 807, anordc 863, or ianordc 799. 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 657 | . . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑) | |
2 | pm2.46 658 | . . 3 ⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓) | |
3 | 1, 2 | jca 290 | . 2 ⊢ (¬ (𝜑 ∨ 𝜓) → (¬ 𝜑 ∧ ¬ 𝜓)) |
4 | simpl 102 | . . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜑) | |
5 | 4 | con2i 557 | . . . 4 ⊢ (𝜑 → ¬ (¬ 𝜑 ∧ ¬ 𝜓)) |
6 | simpr 103 | . . . . 5 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ 𝜓) | |
7 | 6 | con2i 557 | . . . 4 ⊢ (𝜓 → ¬ (¬ 𝜑 ∧ ¬ 𝜓)) |
8 | 5, 7 | jaoi 636 | . . 3 ⊢ ((𝜑 ∨ 𝜓) → ¬ (¬ 𝜑 ∧ ¬ 𝜓)) |
9 | 8 | con2i 557 | . 2 ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 ∨ 𝜓)) |
10 | 3, 9 | impbii 117 | 1 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∧ wa 97 ↔ wb 98 ∨ wo 629 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 630 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm4.56 806 dcor 843 3ioran 900 3ori 1195 unssdif 3172 difundi 3189 sotricim 4060 sotritrieq 4062 en2lp 4278 poxp 5853 nntri2 6073 aptipr 6739 lttri3 7098 letr 7101 apirr 7596 apti 7613 elnnz 8255 xrlttri3 8718 xrletr 8724 expival 9257 nnexmid 9899 |
Copyright terms: Public domain | W3C validator |