Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005)
Ref | Expression | ||
---|---|---|---|
Hypothesis | intnand.1 | ⊢ ( 𝜑 → ¬ 𝜓 ) | |
Assertion | intnanrd | ⊢ ( 𝜑 → ¬ ( 𝜓 ∧ 𝜒 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | intnand.1 | ⊢ ( 𝜑 → ¬ 𝜓 ) | |
2 | simpl | ⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜓 ) | |
3 | 1 2 | nsyl | ⊢ ( 𝜑 → ¬ ( 𝜓 ∧ 𝜒 ) ) |