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

Theorem imnani 391
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 390 . 2 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
31, 2mpbir 223 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 386
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 199  df-an 387
This theorem is referenced by:  mptnan  1812  eueq3  3593  onuninsuci  7320  sucprcreg  8797  elnotel  8804  alephsucdom  9237  pwfseq  9823  eirr  15346  mreexmrid  16700  dvferm1  24196  dvferm2  24198  dchrisumn0  25679  rpvmasum  25684  cvnsym  29738  ballotlem2  31157  bnj1224  31479  bnj1541  31533  bnj1311  31699  bj-imn3ani  33159
  Copyright terms: Public domain W3C validator