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  1769  eueq3  3667  onuninsuci  7780  infn0  9200  sucprcreg  9507  elnotel  9517  alephsucdom  9987  pwfseq  10573  eirr  16128  mreexmrid  17564  dvferm1  25943  dvferm2  25945  dchrisumn0  27486  rpvmasum  27491  cvnsym  32314  ballotlem2  34595  bnj1224  34906  bnj1541  34961  bnj1311  35129  fineqvinfep  35230  bj-imn3ani  36730