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

Theorem imnani 401
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 400 . 2 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
31, 2mpbir 230 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396
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 397
This theorem is referenced by:  mptnan  1769  eueq3  3657  onuninsuci  7755  infn0  9173  sucprcreg  9459  elnotel  9468  alephsucdom  9937  pwfseq  10522  eirr  16014  mreexmrid  17450  dvferm1  25256  dvferm2  25258  dchrisumn0  26776  rpvmasum  26781  cvnsym  30941  ballotlem2  32755  bnj1224  33080  bnj1541  33135  bnj1311  33303  bj-imn3ani  34908
  Copyright terms: Public domain W3C validator