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  7851  infn0  9294  sucprcregOLD  9601  elnotel  9611  alephsucdom  10158  pwfseq  10749  eirr  16373  mreexmrid  17817  dvferm1  26305  dvferm2  26307  dchrisumn0  27848  rpvmasum  27853  cvnsym  32892  ballotlem2  35121  bnj1224  35431  bnj1541  35486  bnj1311  35654  fineqvinfep  35793  bj-imn3ani  37457