![]() |
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 3454 disj 3473 minel 3486 disjsn 3656 sotricim 4325 poirr2 5023 funun 5262 imadiflem 5297 imadif 5298 brprcneu 5510 2omotaplemap 7259 prltlu 7489 caucvgprlemnbj 7669 caucvgprprlemnbj 7695 suplocexprlemmu 7720 xrltnsym2 9797 fzp1nel 10107 fsumsplit 11418 sumsplitdc 11443 phiprmpw 12225 odzdvds 12248 pcdvdsb 12322 lgsne0 14600 bj-nnor 14647 |
Copyright terms: Public domain | W3C validator |