![]() |
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 637 | . . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓))) | |
2 | 1 | imp 124 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓)) |
3 | 2 | con2i 627 | . 2 ⊢ ((𝜑 → ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓)) |
4 | pm3.2 139 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
5 | 4 | con3rr3 633 | . 2 ⊢ (¬ (𝜑 ∧ 𝜓) → (𝜑 → ¬ 𝜓)) |
6 | 3, 5 | impbii 126 | 1 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: imnani 691 nan 692 pm3.24 693 imanst 888 ianordc 899 pm5.17dc 904 dn1dc 960 xorbin 1384 xordc1 1393 alinexa 1603 dfrex2dc 2468 ralinexa 2504 rabeq0 3452 disj 3471 minel 3484 disjsn 3654 sotricim 4323 poirr2 5021 funun 5260 imadiflem 5295 imadif 5296 brprcneu 5508 2omotaplemap 7255 prltlu 7485 caucvgprlemnbj 7665 caucvgprprlemnbj 7691 suplocexprlemmu 7716 xrltnsym2 9793 fzp1nel 10103 fsumsplit 11414 sumsplitdc 11439 phiprmpw 12221 odzdvds 12244 pcdvdsb 12318 lgsne0 14409 bj-nnor 14456 |
Copyright terms: Public domain | W3C validator |