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

Theorem imnani 399
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 398 . 2 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
31, 2mpbir 230 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394
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 206  df-an 395
This theorem is referenced by:  mptnan  1762  eueq3  3703  onuninsuci  7845  infn0  9335  sucprcreg  9631  elnotel  9640  alephsucdom  10109  pwfseq  10694  eirr  16193  mreexmrid  17642  dvferm1  25978  dvferm2  25980  dchrisumn0  27519  rpvmasum  27524  cvnsym  32192  ballotlem2  34259  bnj1224  34583  bnj1541  34638  bnj1311  34806  bj-imn3ani  36215
  Copyright terms: Public domain W3C validator