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

Theorem imnani 400
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
StepHypRef Expression
1 imnani.1 . 2 ¬ (𝜑𝜓)
2 imnan 399 . 2 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
31, 2mpbir 231 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  mptnan  1768  eueq3  3717  onuninsuci  7861  infn0  9340  sucprcreg  9641  elnotel  9650  alephsucdom  10119  pwfseq  10704  eirr  16241  mreexmrid  17686  dvferm1  26023  dvferm2  26025  dchrisumn0  27565  rpvmasum  27570  cvnsym  32309  ballotlem2  34491  bnj1224  34815  bnj1541  34870  bnj1311  35038  bj-imn3ani  36588
  Copyright terms: Public domain W3C validator