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  2953  onuninsuci  4647  alephsucdom  7722  pwfseq  8302  eirr  12499  mreexmrid  13561  dvferm1  19348  dvferm2  19350  dchrisumn0  20686  rpvmasum  20691  cvnsym  22886  ballotlem2  23063  bnj1224  29150  bnj1541  29204  bnj1311  29370
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