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  3669  onuninsuci  7782  infn0  9202  sucprcreg  9509  elnotel  9519  alephsucdom  9989  pwfseq  10575  eirr  16130  mreexmrid  17566  dvferm1  25945  dvferm2  25947  dchrisumn0  27488  rpvmasum  27493  cvnsym  32365  ballotlem2  34646  bnj1224  34957  bnj1541  35012  bnj1311  35180  fineqvinfep  35281  bj-imn3ani  36787