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  2512  necon1bbid  2513  onmindif  4498  ondif2  6517  cnpart  11741  sadadd2lem2  12657  isnirred  15498  isreg2  17121  kqcldsat  17440  trufil  17621  itg2cnlem2  19133  issqf  20390  pjnorm2  22322  atdmd  22994  atmd2  22996  eupath2lem3  23918  dfrdg4  24560  domtri3  25208  dalawlem13  30694
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