![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > annim | Structured version Visualization version GIF version |
Description: Express conjunction in terms of implication. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
annim | ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iman 388 | . 2 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) | |
2 | 1 | con2bii 346 | 1 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 382 |
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 197 df-an 383 |
This theorem is referenced by: pm4.61 391 pm4.52 965 xordi 997 dfifp6 1055 exanali 1937 sbn 2538 r19.35 3232 difin0ss 4093 ordsssuc2 5957 tfindsg 7207 findsg 7240 isf34lem4 9401 hashfun 13426 isprm5 15626 mdetunilem8 20643 4cycl2vnunb 27472 strlem6 29455 hstrlem6 29463 axacprim 31922 ceqsralv2 31945 dfrdg4 32395 andnand1 32735 relowlpssretop 33549 poimirlem1 33743 poimir 33775 2exanali 39113 limsupre2lem 40474 aifftbifffaibif 41608 |
Copyright terms: Public domain | W3C validator |