Theorem imnani 405

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

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

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 401

This theorem is referenced by:  mptnan  1798  eueq3  3674  onuninsuci  7832  infn0  9258  sucprcregOLD  9565  elnotel  9575  alephsucdom  10059  pwfseq  10644  eirr  16256  mreexmrid  17694  dvferm1  26144  dvferm2  26146  dchrisumn0  27685  rpvmasum  27690  cvnsym  32642  ballotlem2  34879  bnj1224  35189  bnj1541  35244  bnj1311  35412  fineqvinfep  35538  bj-imn3ani  37200