Theorem imnani 391

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

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

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 199  df-an 387

This theorem is referenced by:  mptnan  1812  eueq3  3593  onuninsuci  7320  sucprcreg  8797  elnotel  8804  alephsucdom  9237  pwfseq  9823  eirr  15346  mreexmrid  16700  dvferm1  24196  dvferm2  24198  dchrisumn0  25679  rpvmasum  25684  cvnsym  29738  ballotlem2  31157  bnj1224  31479  bnj1541  31533  bnj1311  31699  bj-imn3ani  33159