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

Theorem con1bid 328
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 327 . 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  354  necon1abidOLD  2703  necon1bbid  2704  onmindif  4956  ondif2  7144  cnpart  13155  sadadd2lem2  14184  isnirred  17544  isreg2  20045  kqcldsat  20400  trufil  20577  itg2cnlem2  22335  issqf  23608  eupath2lem3  25181  pjnorm2  26843  atdmd  27515  atmd2  27517  dfrdg4  29828  dalawlem13  36004
  Copyright terms: Public domain W3C validator