Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm3.14 | GIF version |
Description: Theorem *3.14 of [WhiteheadRussell] p. 111. One direction of De Morgan's law). The biconditional holds for decidable propositions as seen at ianordc 799. The converse holds for decidable propositions, as seen at pm3.13dc 866. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Ref | Expression |
---|---|
pm3.14 | ⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 102 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | con3i 562 | . 2 ⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓)) |
3 | simpr 103 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
4 | 3 | con3i 562 | . 2 ⊢ (¬ 𝜓 → ¬ (𝜑 ∧ 𝜓)) |
5 | 2, 4 | jaoi 636 | 1 ⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 97 ∨ 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: pm3.1 671 xoranor 1268 difindiss 3191 |
Copyright terms: Public domain | W3C validator |