imnan - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > imnan		GIF version

Theorem imnan 411

Description: Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.)

**Assertion**
Ref	Expression
imnan	⊢ ((φ → ¬ ψ) ↔ ¬ (φ ∧ ψ))

**Proof of Theorem 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