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

Theorem imnani 413
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 412 . 2  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
31, 2mpbir 201 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359
This theorem is referenced by:  mpto1  1542  eueq3  3109  onuninsuci  4820  alephsucdom  7960  pwfseq  8539  eirr  12804  mreexmrid  13868  dvferm1  19869  dvferm2  19871  dchrisumn0  21215  rpvmasum  21220  cvnsym  23793  ballotlem2  24746  bnj1224  29173  bnj1541  29227  bnj1311  29393
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 178  df-an 361
  Copyright terms: Public domain W3C validator