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 234	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 210  df-an 400

This theorem is referenced by:  mptnan  1776  eueq3  3624  onuninsuci  7619  sucprcreg  9217  elnotel  9225  alephsucdom  9693  pwfseq  10278  eirr  15766  mreexmrid  17146  dvferm1  24882  dvferm2  24884  dchrisumn0  26402  rpvmasum  26407  cvnsym  30371  ballotlem2  32167  bnj1224  32494  bnj1541  32549  bnj1311  32717  bj-imn3ani  34506