Theorem 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	⊢ ¬ ( 𝜑 → ( 𝜓 ∧ 𝜒 ) )
Assertion	nabctnabc	⊢ ( ¬ 𝜑 → ( 𝜓 ∧ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		nabctnabc.1	⊢ ¬ ( 𝜑 → ( 𝜓 ∧ 𝜒 ) )
2		pm4.61	⊢ ( ¬ ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) ↔ ( 𝜑 ∧ ¬ ( 𝜓 ∧ 𝜒 ) ) )
3	2	biimpi	⊢ ( ¬ ( 𝜑 → ( 𝜓 ∧ 𝜒 ) ) → ( 𝜑 ∧ ¬ ( 𝜓 ∧ 𝜒 ) ) )
4	1 3	ax-mp	⊢ ( 𝜑 ∧ ¬ ( 𝜓 ∧ 𝜒 ) )
5	4	simpli	⊢ 𝜑
6	4	simpri	⊢ ¬ ( 𝜓 ∧ 𝜒 )
7	5 6	2th	⊢ ( 𝜑 ↔ ¬ ( 𝜓 ∧ 𝜒 ) )
8		bicom	⊢ ( ( 𝜑 ↔ ¬ ( 𝜓 ∧ 𝜒 ) ) ↔ ( ¬ ( 𝜓 ∧ 𝜒 ) ↔ 𝜑 ) )
9	8	biimpi	⊢ ( ( 𝜑 ↔ ¬ ( 𝜓 ∧ 𝜒 ) ) → ( ¬ ( 𝜓 ∧ 𝜒 ) ↔ 𝜑 ) )
10	7 9	ax-mp	⊢ ( ¬ ( 𝜓 ∧ 𝜒 ) ↔ 𝜑 )
11	10	biimpi	⊢ ( ¬ ( 𝜓 ∧ 𝜒 ) → 𝜑 )
12	11	con3i	⊢ ( ¬ 𝜑 → ¬ ¬ ( 𝜓 ∧ 𝜒 ) )
13	12	notnotrd	⊢ ( ¬ 𝜑 → ( 𝜓 ∧ 𝜒 ) )