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

Theorem con1bid 336
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 206 . . 3  |-  ( ph  ->  ( ch  <->  -.  ps )
)
32con2bid 335 . 2  |-  ( ph  ->  ( ps  <->  -.  ch )
)
43bicomd 206 1  |-  ( ph  ->  ( -.  ch  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  pm5.18  362  necon1bbid  2663  onmindif  5491  ondif2  7191  cnpart  13314  sadadd2lem2  14435  isnirred  17939  isreg2  20404  kqcldsat  20759  trufil  20936  itg2cnlem2  22732  issqf  24075  eupath2lem3  25719  pjnorm2  27392  atdmd  28063  atmd2  28065  dfrdg4  30724  dalawlem13  33450
  Copyright terms: Public domain W3C validator