![]() |
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 986 xordi 1018 dfifp6 1068 exanali 1857 2exanali 1858 ceqsralbv 3657 difin0ss 4379 ordsssuc2 6477 tfindsg 7882 findsg 7920 hashfun 14473 isprm5 16741 mdetunilem8 22641 4cycl2vnunb 30319 mxidlirred 33480 axacprim 35687 dfrdg4 35933 andnand1 36384 relowlpssretop 37347 nlpineqsn 37391 poimirlem1 37608 poimir 37640 fimgmcyc 42521 ralopabb 43401 rexanuz2nf 45443 limsupre2lem 45680 aifftbifffaibif 46871 nfermltl8rev 47667 nfermltl2rev 47668 |
Copyright terms: Public domain | W3C validator |