Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  imnani Structured version   Visualization version   GIF version

Theorem imnani 438
 Description: Infer implication from negated conjunction. (Contributed by Mario Carneiro, 28-Sep-2015.)
Hypothesis
Ref Expression
imnani.1 ¬ (𝜑𝜓)
Assertion
Ref Expression
imnani (𝜑 → ¬ 𝜓)

Proof of Theorem imnani
StepHypRef Expression
1 imnani.1 . 2 ¬ (𝜑𝜓)
2 imnan 437 . 2 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
31, 2mpbir 221 1 (𝜑 → ¬ 𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383 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 197  df-an 385 This theorem is referenced by:  mptnan  1733  eueq3  3414  onuninsuci  7082  sucprcreg  8544  alephsucdom  8940  pwfseq  9524  eirr  14977  mreexmrid  16350  dvferm1  23793  dvferm2  23795  dchrisumn0  25255  rpvmasum  25260  cvnsym  29277  ballotlem2  30678  bnj1224  30998  bnj1541  31052  bnj1311  31218  bj-imn3ani  32697
 Copyright terms: Public domain W3C validator