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

Theorem con2bid 319
Description: A contraposition deduction. (Contributed by NM, 15-Apr-1995.)
Hypothesis
Ref Expression
con2bid.1  |-  ( ph  ->  ( ps  <->  -.  ch )
)
Assertion
Ref Expression
con2bid  |-  ( ph  ->  ( ch  <->  -.  ps )
)

Proof of Theorem con2bid
StepHypRef Expression
1 con2bid.1 . 2  |-  ( ph  ->  ( ps  <->  -.  ch )
)
2 con2bi 318 . 2  |-  ( ( ch  <->  -.  ps )  <->  ( ps  <->  -.  ch )
)
31, 2sylibr 203 1  |-  ( ph  ->  ( ch  <->  -.  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  con1bid  320  necon2abid  2503  necon2bbid  2504  r19.9rzv  3548  sotric  4340  sotrieq  4341  sotr2  4343  isso2i  4346  ordtri2  4427  ordintdif  4441  ord0eln0  4446  ordunisuc2  4635  limsssuc  4641  nlimon  4642  sotri2  5072  sotri3  5073  somin1  5079  somincom  5080  iotanul  5234  soisoi  5825  weniso  5852  tfrlem15  6408  oawordeulem  6552  nnawordex  6635  onomeneq  7050  fimaxg  7104  suplub2  7212  wemapso2lem  7265  cantnflem1  7391  rankval3b  7498  cardsdomel  7607  harsdom  7628  isfin1-2  8011  fin1a2lem7  8032  suplem2pr  8677  xrltnle  8891  ltnle  8902  leloe  8908  xrlttri  10473  xrleloe  10478  xrrebnd  10497  supxrbnd2  10641  supxrbnd  10647  om2uzf1oi  11016  cnpart  11725  bits0e  12620  bitsmod  12627  bitsinv1lem  12632  sadcaddlem  12648  trfil2  17582  xrsxmet  18315  metdsge  18353  ovolunlem1a  18855  ovolunlem1  18856  itg2seq  19097  nodenselem7  24341  finminlem  26231  heiborlem10  26544  stoweidlem34  27783
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