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	⊢ ¬ ( 𝜑 → 𝜓 )
	twonotinotbothi.2	⊢ ¬ ( 𝜒 → 𝜃 )
Assertion	twonotinotbothi	⊢ ¬ ( ( 𝜑 → 𝜓 ) ∧ ( 𝜒 → 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		twonotinotbothi.1	⊢ ¬ ( 𝜑 → 𝜓 )
2		twonotinotbothi.2	⊢ ¬ ( 𝜒 → 𝜃 )
3	1	orci	⊢ ( ¬ ( 𝜑 → 𝜓 ) ∨ ¬ ( 𝜒 → 𝜃 ) )
4		pm3.14	⊢ ( ( ¬ ( 𝜑 → 𝜓 ) ∨ ¬ ( 𝜒 → 𝜃 ) ) → ¬ ( ( 𝜑 → 𝜓 ) ∧ ( 𝜒 → 𝜃 ) ) )
5	3 4	ax-mp	⊢ ¬ ( ( 𝜑 → 𝜓 ) ∧ ( 𝜒 → 𝜃 ) )