Theorem notornotel1

Description: A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018)

	Ref	Expression
Hypothesis	notornotel1.1	$$⊢\phi \to \neg \left(\neg \psi \vee \chi \right)$$
Assertion	notornotel1	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		notornotel1.1	$$⊢\phi \to \neg \left(\neg \psi \vee \chi \right)$$
2		ioran	$$⊢\neg \left(\neg \psi \vee \chi \right)\leftrightarrow \left(\neg \neg \psi \wedge \neg \chi \right)$$
3	2	biimpi	$$⊢\neg \left(\neg \psi \vee \chi \right)\to \left(\neg \neg \psi \wedge \neg \chi \right)$$
4		simpl	$$⊢\left(\neg \neg \psi \wedge \neg \chi \right)\to \neg \neg \psi$$
5		notnotr	$$⊢\neg \neg \psi \to \psi$$
6	3 4 5	3syl	$$⊢\neg \left(\neg \psi \vee \chi \right)\to \psi$$
7	1 6	syl	$$⊢\phi \to \psi$$