Theorem imnani 406

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mptnan  1801  eueq3  3669  onuninsuci  7837  infn0  9273  sucprcregOLD  9580  elnotel  9590  alephsucdom  10083  pwfseq  10674  eirr  16294  mreexmrid  17732  dvferm1  26213  dvferm2  26215  dchrisumn0  27758  rpvmasum  27763  cvnsym  32772  ballotlem2  35001  bnj1224  35311  bnj1541  35366  bnj1311  35534  fineqvinfep  35652  bj-imn3ani  37289