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

Theorem con1bid 320
Description: A contraposition deduction. (Contributed by NM, 9-Oct-1999.)
Hypothesis
Ref Expression
con1bid.1  |-  ( ph  ->  ( -.  ps  <->  ch )
)
Assertion
Ref Expression
con1bid  |-  ( ph  ->  ( -.  ch  <->  ps )
)

Proof of Theorem con1bid
StepHypRef Expression
1 con1bid.1 . . . 4  |-  ( ph  ->  ( -.  ps  <->  ch )
)
21bicomd 192 . . 3  |-  ( ph  ->  ( ch  <->  -.  ps )
)
32con2bid 319 . 2  |-  ( ph  ->  ( ps  <->  -.  ch )
)
43bicomd 192 1  |-  ( ph  ->  ( -.  ch  <->  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  pm5.18  345  necon1abid  2499  necon1bbid  2500  onmindif  4482  ondif2  6501  cnpart  11725  sadadd2lem2  12641  isnirred  15482  isreg2  17105  kqcldsat  17424  trufil  17605  itg2cnlem2  19117  issqf  20374  pjnorm2  22306  atdmd  22978  atmd2  22980  eupath2lem3  23903  dfrdg4  24488  domtri3  25105  dalawlem13  30072
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
  Copyright terms: Public domain W3C validator