nabctnabc

Description: not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ). (Contributed by Jarvin Udandy, 7-Sep-2020)

		Ref	Expression
	Hypothesis	nabctnabc.1	$⊢ \neg (φ \to (ψ \land χ))$
	Assertion	nabctnabc	$⊢ \neg φ \to (ψ \land χ)$

Step	Hyp	Ref	Expression
1		nabctnabc.1	$⊢ \neg (φ \to (ψ \land χ))$
2		pm4.61	$⊢ \neg (φ \to (ψ \land χ)) \leftrightarrow (φ \land \neg (ψ \land χ))$
3	2	biimpi	$⊢ \neg (φ \to (ψ \land χ)) \to (φ \land \neg (ψ \land χ))$
4	1 3	ax-mp	$⊢ (φ \land \neg (ψ \land χ))$
5	4	simpli	$⊢ φ$
6	4	simpri	$⊢ \neg (ψ \land χ)$
7	5 6	2th	$⊢ φ \leftrightarrow \neg (ψ \land χ)$
8		bicom	$⊢ (φ \leftrightarrow \neg (ψ \land χ)) \leftrightarrow (\neg (ψ \land χ) \leftrightarrow φ)$
9	8	biimpi	$⊢ (φ \leftrightarrow \neg (ψ \land χ)) \to (\neg (ψ \land χ) \leftrightarrow φ)$
10	7 9	ax-mp	$⊢ \neg (ψ \land χ) \leftrightarrow φ$
11	10	biimpi	$⊢ \neg (ψ \land χ) \to φ$
12	11	con3i	$⊢ \neg φ \to \neg \neg (ψ \land χ)$
13	12	notnotrd	$⊢ \neg φ \to (ψ \land χ)$

Metamath Proof Explorer