Theorem imnani 402

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

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

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 398

This theorem is referenced by:  mptnan  1770  eueq3  3660  onuninsuci  7758  infn0  9176  sucprcreg  9462  elnotel  9471  alephsucdom  9940  pwfseq  10525  eirr  16013  mreexmrid  17449  dvferm1  25254  dvferm2  25256  dchrisumn0  26774  rpvmasum  26779  cvnsym  30939  ballotlem2  32753  bnj1224  33078  bnj1541  33133  bnj1311  33301  bj-imn3ani  34906