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 230	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 206  df-an 396

This theorem is referenced by:  mptnan  1774  eueq3  3649  onuninsuci  7675  sucprcreg  9321  elnotel  9329  alephsucdom  9819  pwfseq  10404  eirr  15895  mreexmrid  17333  dvferm1  25130  dvferm2  25132  dchrisumn0  26650  rpvmasum  26655  cvnsym  30631  ballotlem2  32434  bnj1224  32760  bnj1541  32815  bnj1311  32983  bj-imn3ani  34748