Theorem imnani 404

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 403	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))
3	1, 2	mpbir 233	1 ⊢ (𝜑 → ¬ 𝜓)

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

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 400

This theorem is referenced by:  mptnan  1788  eueq3  3674  onuninsuci  7820  infn0  9246  sucprcregOLD  9555  elnotel  9565  alephsucdom  10035  pwfseq  10622  eirr  16237  mreexmrid  17675  dvferm1  26047  dvferm2  26049  dchrisumn0  27585  rpvmasum  27590  cvnsym  32493  ballotlem2  34786  bnj1224  35096  bnj1541  35151  bnj1311  35319  fineqvinfep  35421  bj-imn3ani  37030