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 402 | . 2 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) | |
2 | 1 | con2bii 359 | 1 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: pm4.61 405 pm4.52 978 xordi 1010 dfifp6 1060 exanali 1850 2exanali 1851 sbnOLD 2537 sbnALT 2591 difin0ss 4327 ordsssuc2 6273 tfindsg 7563 findsg 7597 hashfun 13788 isprm5 16041 mdetunilem8 21158 4cycl2vnunb 27997 axacprim 32831 ceqsralv2 32854 dfrdg4 33310 andnand1 33647 relowlpssretop 34528 nlpineqsn 34572 poimirlem1 34775 poimir 34807 limsupre2lem 41885 aifftbifffaibif 43038 nfermltl8rev 43754 nfermltl2rev 43755 |
Copyright terms: Public domain | W3C validator |