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

Theorem imnani 424
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 423 . 2  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
31, 2mpbir 212 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  mptnan  1645  eueq3  3188  onuninsuci  6625  sucprcreg  8067  alephsucdom  8461  pwfseq  9040  eirr  14200  mreexmrid  15492  dvferm1  22879  dvferm2  22881  dchrisumn0  24301  rpvmasum  24306  cvnsym  27885  ballotlem2  29273  bnj1224  29565  bnj1541  29619  bnj1311  29785  bj-imn3ani  31119
  Copyright terms: Public domain W3C validator