Theorem imnani 403

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

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

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 209  df-an 399

This theorem is referenced by:  mptnan  1763  eueq3  3700  onuninsuci  7547  sucprcreg  9057  elnotel  9065  alephsucdom  9497  pwfseq  10078  eirr  15550  mreexmrid  16906  dvferm1  24574  dvferm2  24576  dchrisumn0  26089  rpvmasum  26094  cvnsym  30059  ballotlem2  31739  bnj1224  32066  bnj1541  32121  bnj1311  32289  bj-imn3ani  33914