Theorem onenotinotbothi

Description: From one negated implication it is not the case its nonnegated form and a random others are both true. (Contributed by Jarvin Udandy, 11-Sep-2020)

	Ref	Expression
Hypothesis	onenotinotbothi.1	|- -. ( ph -> ps )
Assertion	onenotinotbothi	|- -. ( ( ph -> ps ) /\ ( ch -> th ) )

Proof

Step	Hyp	Ref	Expression
1		onenotinotbothi.1	|- -. ( ph -> ps )
2	1	orci	|- ( -. ( ph -> ps ) \/ -. ( ch -> th ) )
3		pm3.14	|- ( ( -. ( ph -> ps ) \/ -. ( ch -> th ) ) -> -. ( ( ph -> ps ) /\ ( ch -> th ) ) )
4	2 3	ax-mp	|- -. ( ( ph -> ps ) /\ ( ch -> th ) )