Theorem imnani 400

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

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

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 207  df-an 396

This theorem is referenced by:  mptnan  1768  eueq3  3717  onuninsuci  7861  infn0  9340  sucprcreg  9641  elnotel  9650  alephsucdom  10119  pwfseq  10704  eirr  16241  mreexmrid  17686  dvferm1  26023  dvferm2  26025  dchrisumn0  27565  rpvmasum  27570  cvnsym  32309  ballotlem2  34491  bnj1224  34815  bnj1541  34870  bnj1311  35038  bj-imn3ani  36588