Theorem imnani 400

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

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

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 207  df-an 396

This theorem is referenced by:  mptnan  1770  eueq3  3671  onuninsuci  7792  infn0  9214  sucprcreg  9521  elnotel  9531  alephsucdom  10001  pwfseq  10587  eirr  16142  mreexmrid  17578  dvferm1  25957  dvferm2  25959  dchrisumn0  27500  rpvmasum  27505  cvnsym  32378  ballotlem2  34667  bnj1224  34977  bnj1541  35032  bnj1311  35200  fineqvinfep  35303  bj-imn3ani  36812