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  3658  onuninsuci  7785  infn0  9206  sucprcregOLD  9515  elnotel  9525  alephsucdom  9995  pwfseq  10581  eirr  16166  mreexmrid  17603  dvferm1  25965  dvferm2  25967  dchrisumn0  27501  rpvmasum  27506  cvnsym  32379  ballotlem2  34652  bnj1224  34962  bnj1541  35017  bnj1311  35185  fineqvinfep  35288  bj-imn3ani  36871