Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > imnan | GIF version |
Description: Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.) (Revised by Mario Carneiro, 1-Feb-2015.) |
Ref | Expression |
---|---|
imnan | ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.2im 611 | . . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓))) | |
2 | 1 | imp 123 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓)) |
3 | 2 | con2i 601 | . 2 ⊢ ((𝜑 → ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓)) |
4 | pm3.2 138 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
5 | 4 | con3rr3 607 | . 2 ⊢ (¬ (𝜑 ∧ 𝜓) → (𝜑 → ¬ 𝜓)) |
6 | 3, 5 | impbii 125 | 1 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 |
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 588 ax-in2 589 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: imnani 665 nan 666 pm3.24 667 imanst 858 ianordc 869 pm5.17dc 874 dn1dc 929 xorbin 1347 xordc1 1356 alinexa 1567 dfrex2dc 2405 ralinexa 2439 rabeq0 3362 disj 3381 minel 3394 disjsn 3555 sotricim 4215 poirr2 4901 funun 5137 imadiflem 5172 imadif 5173 brprcneu 5382 prltlu 7263 caucvgprlemnbj 7443 caucvgprprlemnbj 7469 suplocexprlemmu 7494 xrltnsym2 9548 fzp1nel 9852 fsumsplit 11144 sumsplitdc 11169 phiprmpw 11825 bj-nnor 12873 |
Copyright terms: Public domain | W3C validator |