Theorem imnani 403

Description: Infer an implication from a negated conjunction. (Contributed by Mario Carneiro, 28-Sep-2015.)

Hypothesis

Ref	Expression
imnani.1	⊢ ¬ (𝜑 ∧ 𝜓)

Assertion

Ref	Expression
imnani	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem imnani

Step	Hyp	Ref	Expression
1		imnani.1	. 2 ⊢ ¬ (𝜑 ∧ 𝜓)
2		imnan 402	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))
3	1, 2	mpbir 233	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  mptnan  1769  eueq3  3704  onuninsuci  7557  sucprcreg  9067  elnotel  9075  alephsucdom  9507  pwfseq  10088  eirr  15560  mreexmrid  16916  dvferm1  24584  dvferm2  24586  dchrisumn0  26099  rpvmasum  26104  cvnsym  30069  ballotlem2  31748  bnj1224  32075  bnj1541  32130  bnj1311  32298  bj-imn3ani  33923