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 232	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 208  df-an 397

This theorem is referenced by:  mptnan  1775  eueq3  3652  onuninsuci  7780  infn0  9202  sucprcregOLD  9512  elnotel  9522  alephsucdom  9992  pwfseq  10578  eirr  16163  mreexmrid  17600  dvferm1  25970  dvferm2  25972  dchrisumn0  27502  rpvmasum  27507  cvnsym  32379  ballotlem2  34673  bnj1224  34983  bnj1541  35038  bnj1311  35206  fineqvinfep  35306  bj-imn3ani  36898