Theorem conax1k

Description: Weakening of conax1 . General instance of pm2.51 and of pm2.52 . (Contributed by BJ, 28-Oct-2023)

	Ref	Expression
Assertion	conax1k	⊢ ( ¬ ( 𝜑 → 𝜓 ) → ( 𝜒 → ¬ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		conax1	⊢ ( ¬ ( 𝜑 → 𝜓 ) → ¬ 𝜓 )
2	1	a1d	⊢ ( ¬ ( 𝜑 → 𝜓 ) → ( 𝜒 → ¬ 𝜓 ) )