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 884. The converse holds for decidable propositions, as seen at pm3.13dc 943. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Ref | Expression |
---|---|
pm3.14 | ⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 108 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
2 | 1 | con3i 621 | . 2 ⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓)) |
3 | simpr 109 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
4 | 3 | con3i 621 | . 2 ⊢ (¬ 𝜓 → ¬ (𝜑 ∧ 𝜓)) |
5 | 2, 4 | jaoi 705 | 1 ⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ∨ wo 697 |
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 603 ax-in2 604 ax-io 698 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm3.1 743 xoranor 1355 difindiss 3325 |
Copyright terms: Public domain | W3C validator |