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  3676  onuninsuci  7842  infn0  9269  sucprcregOLD  9576  elnotel  9586  alephsucdom  10079  pwfseq  10666  eirr  16285  mreexmrid  17723  dvferm1  26197  dvferm2  26199  dchrisumn0  27738  rpvmasum  27743  cvnsym  32715  ballotlem2  34946  bnj1224  35256  bnj1541  35311  bnj1311  35479  fineqvinfep  35597  bj-imn3ani  37239