nandsym1

		Ref	Expression
	Assertion	nandsym1	$⊢ (ψ ⊼ (ψ ⊼ ⊥)) \to (ψ ⊼ φ)$

Step	Hyp	Ref	Expression
1		df-nan	$⊢ (ψ ⊼ (ψ ⊼ ⊥)) \leftrightarrow \neg (ψ \land (ψ ⊼ ⊥))$
2	1	biimpi	$⊢ (ψ ⊼ (ψ ⊼ ⊥)) \to \neg (ψ \land (ψ ⊼ ⊥))$
3		df-nan	$⊢ (ψ ⊼ ⊥) \leftrightarrow \neg (ψ \land ⊥)$
4	3	anbi2i	$⊢ (ψ \land (ψ ⊼ ⊥)) \leftrightarrow (ψ \land \neg (ψ \land ⊥))$
5	2 4	sylnib	$⊢ (ψ ⊼ (ψ ⊼ ⊥)) \to \neg (ψ \land \neg (ψ \land ⊥))$
6		simpl	$⊢ (ψ \land φ) \to ψ$
7		fal	$⊢ \neg ⊥$
8	7	intnan	$⊢ \neg (ψ \land ⊥)$
9	6 8	jctir	$⊢ (ψ \land φ) \to (ψ \land \neg (ψ \land ⊥))$
10	5 9	nsyl	$⊢ (ψ ⊼ (ψ ⊼ ⊥)) \to \neg (ψ \land φ)$
11		df-nan	$⊢ (ψ ⊼ φ) \leftrightarrow \neg (ψ \land φ)$
12	10 11	sylibr	$⊢ (ψ ⊼ (ψ ⊼ ⊥)) \to (ψ ⊼ φ)$

Metamath Proof Explorer