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

Theorem con2bid 320
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 319 . 2  |-  ( ( ch  <->  -.  ps )  <->  ( ps  <->  -.  ch )
)
31, 2sylibr 204 1  |-  ( ph  ->  ( ch  <->  -.  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  con1bid  321  necon2abid  2600  necon2bbid  2601  r19.9rzv  3658  sotric  4463  sotrieq  4464  sotr2  4466  isso2i  4469  ordtri2  4550  ordintdif  4564  ord0eln0  4569  ordunisuc2  4757  limsssuc  4763  nlimon  4764  sotri2  5196  sotri3  5197  somin1  5203  somincom  5204  iotanul  5366  soisoi  5980  weniso  6007  tfrlem15  6582  oawordeulem  6726  nnawordex  6809  onomeneq  7225  fimaxg  7283  suplub2  7392  wemapso2lem  7445  cantnflem1  7571  rankval3b  7678  cardsdomel  7787  harsdom  7808  isfin1-2  8191  fin1a2lem7  8212  suplem2pr  8856  xrltnle  9070  ltnle  9081  leloe  9087  xrlttri  10657  xrleloe  10662  xrrebnd  10681  supxrbnd2  10826  supxrbnd  10832  om2uzf1oi  11213  cnpart  11965  bits0e  12861  bitsmod  12868  bitsinv1lem  12873  sadcaddlem  12889  trfil2  17833  xrsxmet  18704  metdsge  18743  ovolunlem1a  19252  ovolunlem1  19253  itg2seq  19494  gsumesum  24240  nodenselem7  25358  finminlem  26005  heiborlem10  26213
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