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

Theorem imnani 438
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 437 . 2 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
31, 2mpbir 220 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383
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 196  df-an 385
This theorem is referenced by:  mptnan  1684  eueq3  3348  onuninsuci  6932  sucprcreg  8389  alephsucdom  8785  pwfseq  9365  eirr  14772  mreexmrid  16126  dvferm1  23552  dvferm2  23554  dchrisumn0  25010  rpvmasum  25015  cvnsym  28533  ballotlem2  29877  bnj1224  30126  bnj1541  30180  bnj1311  30346  bj-imn3ani  31745
  Copyright terms: Public domain W3C validator