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

Theorem imnani 423
Description: Infer implication from negated conjunction. (Contributed by Mario Carneiro, 28-Sep-2015.)
Hypothesis
Ref Expression
imnani.1  |-  -.  ( ph  /\  ps )
Assertion
Ref Expression
imnani  |-  ( ph  ->  -.  ps )

Proof of Theorem imnani
StepHypRef Expression
1 imnani.1 . 2  |-  -.  ( ph  /\  ps )
2 imnan 422 . 2  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
31, 2mpbir 209 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  mptnan  1576  eueq3  3241  onuninsuci  6564  sucprcreg  7929  alephsucdom  8364  pwfseq  8946  eirr  13609  mreexmrid  14704  dvferm1  21600  dvferm2  21602  dchrisumn0  22913  rpvmasum  22918  cvnsym  25873  ballotlem2  27038  bnj1224  32150  bnj1541  32204  bnj1311  32370  bj-imn3ani  32468
  Copyright terms: Public domain W3C validator