Theorem nsyl2OLD

Description: Obsolete version of nsyl2 as of 14-Nov-2023. (Contributed by NM, 26-Jun-1994) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nsyl2OLD.1	$$⊢\phi \to \neg \psi$$
	nsyl2OLD.2	$$⊢\neg \chi \to \psi$$
Assertion	nsyl2OLD	$$⊢\phi \to \chi$$

Proof

Step	Hyp	Ref	Expression
1		nsyl2OLD.1	$$⊢\phi \to \neg \psi$$
2		nsyl2OLD.2	$$⊢\neg \chi \to \psi$$
3	2	a1i	$$⊢\phi \to \left(\neg \chi \to \psi \right)$$
4	1 3	mt3d	$$⊢\phi \to \chi$$