![]() |
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 400 | . 2 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) | |
2 | 1 | con2bii 356 | 1 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 |
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 206 df-an 395 |
This theorem is referenced by: pm4.61 403 pm4.52 982 xordi 1014 dfifp6 1066 exanali 1854 2exanali 1855 ceqsralbv 3645 difin0ss 4372 ordsssuc2 6465 tfindsg 7871 findsg 7911 hashfun 14436 isprm5 16685 mdetunilem8 22541 4cycl2vnunb 30120 mxidlirred 33210 axacprim 35334 dfrdg4 35580 andnand1 35918 relowlpssretop 36876 nlpineqsn 36920 poimirlem1 37127 poimir 37159 ralopabb 42872 rexanuz2nf 44904 limsupre2lem 45141 aifftbifffaibif 46332 nfermltl8rev 47111 nfermltl2rev 47112 |
Copyright terms: Public domain | W3C validator |