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

Theorem imnani 404
 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 403 . 2 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
31, 2mpbir 234 1 (𝜑 → ¬ 𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  mptnan  1770  eueq3  3650  onuninsuci  7537  sucprcreg  9051  elnotel  9059  alephsucdom  9492  pwfseq  10077  eirr  15552  mreexmrid  16908  dvferm1  24595  dvferm2  24597  dchrisumn0  26112  rpvmasum  26117  cvnsym  30080  ballotlem2  31868  bnj1224  32195  bnj1541  32250  bnj1311  32418  bj-imn3ani  34050
 Copyright terms: Public domain W3C validator