Theorem imnani 438

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

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

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 385

This theorem is referenced by:  mptnan  1733  eueq3  3414  onuninsuci  7082  sucprcreg  8544  alephsucdom  8940  pwfseq  9524  eirr  14977  mreexmrid  16350  dvferm1  23793  dvferm2  23795  dchrisumn0  25255  rpvmasum  25260  cvnsym  29277  ballotlem2  30678  bnj1224  30998  bnj1541  31052  bnj1311  31218  bj-imn3ani  32697