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

Theorem con1bid 330
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 201 . . 3  |-  ( ph  ->  ( ch  <->  -.  ps )
)
32con2bid 329 . 2  |-  ( ph  ->  ( ps  <->  -.  ch )
)
43bicomd 201 1  |-  ( ph  ->  ( -.  ch  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  pm5.18  356  necon1abidOLD  2697  necon1bbid  2698  onmindif  4908  ondif2  7044  cnpart  12833  sadadd2lem2  13750  isnirred  16900  isreg2  19099  kqcldsat  19424  trufil  19601  itg2cnlem2  21358  issqf  22592  eupath2lem3  23737  pjnorm2  25267  atdmd  25939  atmd2  25941  dfrdg4  28117  dalawlem13  33835
  Copyright terms: Public domain W3C validator