Theorem imnani 401

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

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

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 206  df-an 397

This theorem is referenced by:  mptnan  1770  eueq3  3672  onuninsuci  7781  infn0  9258  sucprcreg  9546  elnotel  9555  alephsucdom  10024  pwfseq  10609  eirr  16098  mreexmrid  17537  dvferm1  25386  dvferm2  25388  dchrisumn0  26906  rpvmasum  26911  cvnsym  31295  ballotlem2  33177  bnj1224  33502  bnj1541  33557  bnj1311  33725  bj-imn3ani  35128