pm5.19 - New Foundations Explorer

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

Theorem pm5.19 349

Description: Theorem *5.19 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.)

**Assertion**
Ref	Expression
pm5.19	⊢ ¬ (φ ↔ ¬ φ)

**Proof of Theorem pm5.19**
Step	Hyp	Ref	Expression
1		biid 227	. 2 ⊢ (φ ↔ φ)
2		pm5.18 345	. 2 ⊢ ((φ ↔ φ) ↔ ¬ (φ ↔ ¬ φ))
3	1, 2	mpbi 199	1 ⊢ ¬ (φ ↔ ¬ φ)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 176

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

This theorem is referenced by: ru 3045 necompl 3544 nenpw1pwlem2 6085