notbinot1 - Mathbox for Giovanni Mascellani

	Mathbox for Giovanni Mascellani		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > notbinot1		Structured version Visualization version GIF version

Theorem notbinot1 38045

Description: Simplification rule of negation across a biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.)

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

**Proof of Theorem notbinot1**
Step	Hyp	Ref	Expression
1		nbbn 383	. . 3 ⊢ ((¬ 𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))
2	1	bicomi 224	. 2 ⊢ (¬ (𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ 𝜓))
3	2	con1bii 356	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: bicontr 38046