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

Proof

Step	Hyp	Ref	Expression
1		onenotinotbothi.1	$$⊢\neg \left(\phi \to \psi \right)$$
2	1	orci	$$⊢\left(\neg \left(\phi \to \psi \right)\vee \neg \left(\chi \to \theta \right)\right)$$
3		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)$$
4	2 3	ax-mp	$$⊢\neg \left(\left(\phi \to \psi \right)\wedge \left(\chi \to \theta \right)\right)$$