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, 6Jun2018.)
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  ⊢ ((¬ (𝜑 ∧ 𝜓) ∧ 𝜓) → ¬ 𝜑)

