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  3657  onuninsuci  7791  infn0  9212  sucprcregOLD  9521  elnotel  9531  alephsucdom  10001  pwfseq  10587  eirr  16172  mreexmrid  17609  dvferm1  25952  dvferm2  25954  dchrisumn0  27484  rpvmasum  27489  cvnsym  32361  ballotlem2  34633  bnj1224  34943  bnj1541  34998  bnj1311  35166  fineqvinfep  35269  bj-imn3ani  36852