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

Proof

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