| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > annim | Structured version Visualization version GIF version | ||
| Description: Express a conjunction in terms of a negated implication. (Contributed by NM, 2-Aug-1994.) |
| Ref | Expression |
|---|---|
| annim | ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iman 401 | . 2 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) | |
| 2 | 1 | con2bii 357 | 1 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-an 396 |
| This theorem is referenced by: pm4.61 404 pm4.52 987 xordi 1019 dfifp6 1069 exanali 1859 2exanali 1860 ceqsralbv 3657 difin0ss 4373 ordsssuc2 6475 tfindsg 7882 findsg 7919 hashfun 14476 isprm5 16744 mdetunilem8 22625 4cycl2vnunb 30309 mxidlirred 33500 axacprim 35707 dfrdg4 35952 andnand1 36402 relowlpssretop 37365 nlpineqsn 37409 poimirlem1 37628 poimir 37660 fimgmcyc 42544 ralopabb 43424 rexanuz2nf 45503 limsupre2lem 45739 aifftbifffaibif 46933 nfermltl8rev 47729 nfermltl2rev 47730 |
| Copyright terms: Public domain | W3C validator |