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 626 | . . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓))) | |
2 | 1 | imp 123 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓)) |
3 | 2 | con2i 616 | . 2 ⊢ ((𝜑 → ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓)) |
4 | pm3.2 138 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
5 | 4 | con3rr3 622 | . 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 603 ax-in2 604 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: imnani 680 nan 681 pm3.24 682 imanst 873 ianordc 884 pm5.17dc 889 dn1dc 944 xorbin 1362 xordc1 1371 alinexa 1582 dfrex2dc 2428 ralinexa 2462 rabeq0 3392 disj 3411 minel 3424 disjsn 3585 sotricim 4245 poirr2 4931 funun 5167 imadiflem 5202 imadif 5203 brprcneu 5414 prltlu 7295 caucvgprlemnbj 7475 caucvgprprlemnbj 7501 suplocexprlemmu 7526 xrltnsym2 9580 fzp1nel 9884 fsumsplit 11176 sumsplitdc 11201 phiprmpw 11898 bj-nnor 12946 |
Copyright terms: Public domain | W3C validator |