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

Theorem imnani 439
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 438 . 2 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
31, 2mpbir 221 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384
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 386
This theorem is referenced by:  mptnan  1692  eueq3  3379  onuninsuci  7037  sucprcreg  8503  alephsucdom  8899  pwfseq  9483  eirr  14927  mreexmrid  16297  dvferm1  23742  dvferm2  23744  dchrisumn0  25204  rpvmasum  25209  cvnsym  29133  ballotlem2  30535  bnj1224  30857  bnj1541  30911  bnj1311  31077  bj-imn3ani  32556
  Copyright terms: Public domain W3C validator