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

Theorem con1bid 321
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 193 . . 3  |-  ( ph  ->  ( ch  <->  -.  ps )
)
32con2bid 320 . 2  |-  ( ph  ->  ( ps  <->  -.  ch )
)
43bicomd 193 1  |-  ( ph  ->  ( -.  ch  <->  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  pm5.18  346  necon1abid  2657  necon1bbid  2658  onmindif  4671  ondif2  6746  cnpart  12045  sadadd2lem2  12962  isnirred  15805  isreg2  17441  kqcldsat  17765  trufil  17942  itg2cnlem2  19654  issqf  20919  eupath2lem3  21701  pjnorm2  23229  atdmd  23901  atmd2  23903  dfrdg4  25795  dalawlem13  30680
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
  Copyright terms: Public domain W3C validator