Theorem imnani 439

Description: Infer implication from 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 438	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))
3	1, 2	mpbir 221	1 ⊢ (𝜑 → ¬ 𝜓)

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

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 197  df-an 386

This theorem is referenced by:  mptnan  1693  eueq3  3381  onuninsuci  7040  sucprcreg  8506  alephsucdom  8902  pwfseq  9486  eirr  14933  mreexmrid  16303  dvferm1  23748  dvferm2  23750  dchrisumn0  25210  rpvmasum  25215  cvnsym  29149  ballotlem2  30550  bnj1224  30872  bnj1541  30926  bnj1311  31092  bj-imn3ani  32572