MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con2bid Structured version   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  2655  necon2bbid  2656  r19.9rzv  3714  sotric  4521  sotrieq  4522  sotr2  4524  isso2i  4527  ordtri2  4608  ordintdif  4622  ord0eln0  4627  ordunisuc2  4816  limsssuc  4822  nlimon  4823  sotri2  5255  sotri3  5256  somin1  5262  somincom  5263  iotanul  5425  soisoi  6040  weniso  6067  tfrlem15  6645  oawordeulem  6789  nnawordex  6872  onomeneq  7288  fimaxg  7346  suplub2  7458  wemapso2lem  7511  cantnflem1  7637  rankval3b  7744  cardsdomel  7853  harsdom  7874  isfin1-2  8257  fin1a2lem7  8278  suplem2pr  8922  xrltnle  9136  ltnle  9147  leloe  9153  xrlttri  10724  xrleloe  10729  xrrebnd  10748  supxrbnd2  10893  supxrbnd  10899  om2uzf1oi  11285  cnpart  12037  bits0e  12933  bitsmod  12940  bitsinv1lem  12945  sadcaddlem  12961  trfil2  17911  xrsxmet  18832  metdsge  18871  ovolunlem1a  19384  ovolunlem1  19385  itg2seq  19626  toslub  24183  tosglb  24184  isarchi2  24247  gsumesum  24443  nodenselem7  25634  elfuns  25752  itg2addnclem  26246  finminlem  26312  heiborlem10  26520
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