nbn3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > nbn3		Structured version Visualization version GIF version

Theorem nbn3 373

Description: Transfer falsehood via equivalence. (Contributed by NM, 11-Sep-2006.)

**Hypothesis**
Ref	Expression
nbn3.1	⊢ 𝜑

**Assertion**
Ref	Expression
nbn3	⊢ (¬ 𝜓 ↔ (𝜓 ↔ ¬ 𝜑))

**Proof of Theorem nbn3**
Step	Hyp	Ref	Expression
1		nbn3.1	. . 3 ⊢ 𝜑
2	1	notnoti 143	. 2 ⊢ ¬ ¬ 𝜑
3	2	nbn 372	1 ⊢ (¬ 𝜓 ↔ (𝜓 ↔ ¬ 𝜑))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 206

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

This theorem is referenced by: ab0orv 4363