![]() |
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 392 | . 2 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) | |
2 | 1 | con2bii 349 | 1 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: pm4.61 395 pm4.52 970 xordi 1002 dfifp6 1052 exanali 1904 sbn 2467 r19.35 3270 difin0ss 4177 ordsssuc2 6064 tfindsg 7338 findsg 7371 isf34lem4 9534 hashfun 13538 isprm5 15823 mdetunilem8 20830 4cycl2vnunb 27698 strlem6 29687 hstrlem6 29695 axacprim 32181 ceqsralv2 32204 dfrdg4 32647 andnand1 32984 relowlpssretop 33807 poimirlem1 34036 poimir 34068 2exanali 39543 limsupre2lem 40864 aifftbifffaibif 42015 |
Copyright terms: Public domain | W3C validator |