Theorem twonotinotbothi

Description: From these two negated implications it is not the case their nonnegated forms are both true. (Contributed by Jarvin Udandy, 11-Sep-2020)

	Ref	Expression
Hypotheses	twonotinotbothi.1	|- -. ( ph -> ps )
	twonotinotbothi.2	|- -. ( ch -> th )
Assertion	twonotinotbothi	|- -. ( ( ph -> ps ) /\ ( ch -> th ) )

Proof

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