Description: Weakening of conax1 . General instance of pm2.51 and of pm2.52 . (Contributed by BJ, 28-Oct-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | conax1k | ⊢ ( ¬ ( 𝜑 → 𝜓 ) → ( 𝜒 → ¬ 𝜓 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | conax1 | ⊢ ( ¬ ( 𝜑 → 𝜓 ) → ¬ 𝜓 ) | |
2 | 1 | a1d | ⊢ ( ¬ ( 𝜑 → 𝜓 ) → ( 𝜒 → ¬ 𝜓 ) ) |