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  3672  onuninsuci  7885  infn0  9332  sucprcregOLD  9638  elnotel  9648  alephsucdom  10197  pwfseq  10788  eirr  16417  mreexmrid  17867  dvferm1  26360  dvferm2  26362  dchrisumn0  27905  rpvmasum  27910  cvnsym  32949  ballotlem2  35232  bnj1224  35542  bnj1541  35597  bnj1311  35765  fineqvinfep  35934  bj-imn3ani  37672