Description: If a double conjunction is false and the second conjunct is true, then
the first conjunct is false.
not12an2impnot1VD is the Virtual
Deduction proof verified by automatically transforming it into the
Metamath proof of not12an2impnot1 using completeusersproof, which is
verified by the Metamath program.
not12an2impnot1RO is a form of
the completed proof which preserves the Virtual Deduction proof's step
numbers and their ordering. (Contributed by Alan Sare, 6-Jun-2018.)
Assertion
| Ref
| Expression |
|---|
| not12an2impnot1RO |
⊢ ((¬
(𝜑 ∧ 𝜓) ∧ 𝜓) → ¬ 𝜑) |
Proof of Theorem not12an2impnot1RO
| Step | Hyp | Ref | Expression |
|---|
| 1 | | id | ⊢ ((¬ (𝜑 ∧ 𝜓) ∧ 𝜓) → (¬ (𝜑 ∧ 𝜓) ∧ 𝜓))
| | 2 | 1 | simpld | ⊢ ((¬ (𝜑 ∧ 𝜓) ∧ 𝜓) → ¬ (𝜑 ∧ 𝜓))
| | d2 | | pm3.21 | ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
| | d1 | d2 | con3rr3 | ⊢ (¬ (𝜑 ∧ 𝜓) → (𝜓 → ¬ 𝜑))
| | 3 | 2, d1 | syl | ⊢ ((¬ (𝜑 ∧ 𝜓) ∧ 𝜓) → (𝜓 → ¬ 𝜑))
| | 4 | 1 | simprd | ⊢ ((¬ (𝜑 ∧ 𝜓) ∧ 𝜓) → 𝜓)
| | qed | 4, 3 | mpd | ⊢ ((¬ (𝜑 ∧ 𝜓) ∧ 𝜓) → ¬ 𝜑)
|
|