Theorem imnani 399

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

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

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 395

This theorem is referenced by:  mptnan  1762  eueq3  3703  onuninsuci  7845  infn0  9335  sucprcreg  9631  elnotel  9640  alephsucdom  10109  pwfseq  10694  eirr  16193  mreexmrid  17642  dvferm1  25978  dvferm2  25980  dchrisumn0  27519  rpvmasum  27524  cvnsym  32192  ballotlem2  34259  bnj1224  34583  bnj1541  34638  bnj1311  34806  bj-imn3ani  36215