New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > imnan | GIF version |
Description: Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.) |
Ref | Expression |
---|---|
imnan | ⊢ ((φ → ¬ ψ) ↔ ¬ (φ ∧ ψ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-an 360 | . 2 ⊢ ((φ ∧ ψ) ↔ ¬ (φ → ¬ ψ)) | |
2 | 1 | con2bii 322 | 1 ⊢ ((φ → ¬ ψ) ↔ ¬ (φ ∧ ψ)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 176 ∧ wa 358 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 df-an 360 |
This theorem is referenced by: imnani 412 iman 413 ianor 474 nan 563 pm5.17 858 pm5.16 860 dn1 932 nic-ax 1438 nic-axALT 1439 alinexa 1578 dfsb3 2056 ralinexa 2659 pssn2lp 3370 minel 3606 disjsn 3786 ltfinirr 4457 tfinltfin 4501 evenodddisj 4516 funun 5146 imadif 5171 nmembers1lem2 6269 nmembers1lem3 6270 |
Copyright terms: Public domain | W3C validator |