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	⊢ ( 𝜑 → ¬ 𝜓 )
	nsyl2OLD.2	⊢ ( ¬ 𝜒 → 𝜓 )
Assertion	nsyl2OLD	⊢ ( 𝜑 → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		nsyl2OLD.1	⊢ ( 𝜑 → ¬ 𝜓 )
2		nsyl2OLD.2	⊢ ( ¬ 𝜒 → 𝜓 )
3	2	a1i	⊢ ( 𝜑 → ( ¬ 𝜒 → 𝜓 ) )
4	1 3	mt3d	⊢ ( 𝜑 → 𝜒 )