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  1768  eueq3  3679  onuninsuci  7796  infn0  9227  sucprcreg  9530  elnotel  9539  alephsucdom  10008  pwfseq  10593  eirr  16149  mreexmrid  17580  dvferm1  25865  dvferm2  25867  dchrisumn0  27408  rpvmasum  27413  cvnsym  32192  ballotlem2  34453  bnj1224  34764  bnj1541  34819  bnj1311  34987  bj-imn3ani  36548