Theorem imnani 402

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 401	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))
3	1, 2	mpbir 230	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  mptnan  1771  eueq3  3708  onuninsuci  7829  infn0  9307  sucprcreg  9596  elnotel  9605  alephsucdom  10074  pwfseq  10659  eirr  16148  mreexmrid  17587  dvferm1  25502  dvferm2  25504  dchrisumn0  27024  rpvmasum  27029  cvnsym  31574  ballotlem2  33518  bnj1224  33843  bnj1541  33898  bnj1311  34066  bj-imn3ani  35513