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	$$⊢\neg \left(\phi \to \psi \right)$$
	twonotinotbothi.2	$$⊢\neg \left(\chi \to \theta \right)$$
Assertion	twonotinotbothi	$$⊢\neg \left(\left(\phi \to \psi \right)\wedge \left(\chi \to \theta \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		twonotinotbothi.1	$$⊢\neg \left(\phi \to \psi \right)$$
2		twonotinotbothi.2	$$⊢\neg \left(\chi \to \theta \right)$$
3	1	orci	$$⊢\left(\neg \left(\phi \to \psi \right)\vee \neg \left(\chi \to \theta \right)\right)$$
4		pm3.14	$$⊢\left(\neg \left(\phi \to \psi \right)\vee \neg \left(\chi \to \theta \right)\right)\to \neg \left(\left(\phi \to \psi \right)\wedge \left(\chi \to \theta \right)\right)$$
5	3 4	ax-mp	$$⊢\neg \left(\left(\phi \to \psi \right)\wedge \left(\chi \to \theta \right)\right)$$