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  1800  eueq3  3668  onuninsuci  7855  infn0  9302  sucprcregOLD  9608  elnotel  9618  alephsucdom  10165  pwfseq  10756  eirr  16382  mreexmrid  17826  dvferm1  26314  dvferm2  26316  dchrisumn0  27857  rpvmasum  27862  cvnsym  32901  ballotlem2  35171  bnj1224  35481  bnj1541  35536  bnj1311  35704  fineqvinfep  35861  bj-imn3ani  37581