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	|- -. ( ph -> ( ps /\ ch ) )
Assertion	nabctnabc	|- ( -. ph -> ( ps /\ ch ) )

Proof

Step	Hyp	Ref	Expression
1		nabctnabc.1	|- -. ( ph -> ( ps /\ ch ) )
2		pm4.61	|- ( -. ( ph -> ( ps /\ ch ) ) <-> ( ph /\ -. ( ps /\ ch ) ) )
3	2	biimpi	|- ( -. ( ph -> ( ps /\ ch ) ) -> ( ph /\ -. ( ps /\ ch ) ) )
4	1 3	ax-mp	|- ( ph /\ -. ( ps /\ ch ) )
5	4	simpli	|- ph
6	4	simpri	|- -. ( ps /\ ch )
7	5 6	2th	|- ( ph <-> -. ( ps /\ ch ) )
8		bicom	|- ( ( ph <-> -. ( ps /\ ch ) ) <-> ( -. ( ps /\ ch ) <-> ph ) )
9	8	biimpi	|- ( ( ph <-> -. ( ps /\ ch ) ) -> ( -. ( ps /\ ch ) <-> ph ) )
10	7 9	ax-mp	|- ( -. ( ps /\ ch ) <-> ph )
11	10	biimpi	|- ( -. ( ps /\ ch ) -> ph )
12	11	con3i	|- ( -. ph -> -. -. ( ps /\ ch ) )
13	12	notnotrd	|- ( -. ph -> ( ps /\ ch ) )