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  1585  eueq3  3283  onuninsuci  6670  sucprcreg  8037  alephsucdom  8472  pwfseq  9054  eirr  13816  mreexmrid  14915  dvferm1  22254  dvferm2  22256  dchrisumn0  23572  rpvmasum  23577  cvnsym  27032  ballotlem2  28252  bnj1224  33340  bnj1541  33394  bnj1311  33560  bj-imn3ani  33658
  Copyright terms: Public domain W3C validator