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

Theorem imnani 412
Description: Express implication in terms of 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 411 . 2  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
31, 2mpbir 200 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358
This theorem is referenced by:  mpto1  1523  eueq3  2940  onuninsuci  4631  alephsucdom  7706  pwfseq  8286  eirr  12483  mreexmrid  13545  dvferm1  19332  dvferm2  19334  dchrisumn0  20670  rpvmasum  20675  cvnsym  22870  ballotlem2  23047  bnj1224  28834  bnj1541  28888  bnj1311  29054
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator