Theorem imnani 405

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

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

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 210  df-an 401

This theorem is referenced by:  mptnan  1795  eueq3  3683  onuninsuci  7836  infn0  9262  sucprcregOLD  9569  elnotel  9579  alephsucdom  10063  pwfseq  10649  eirr  16261  mreexmrid  17699  dvferm1  26113  dvferm2  26115  dchrisumn0  27651  rpvmasum  27656  cvnsym  32583  ballotlem2  34824  bnj1224  35134  bnj1541  35189  bnj1311  35357  fineqvinfep  35461  bj-imn3ani  37069