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

Theorem con2bid 330
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 329 . 2  |-  ( ( ch  <->  -.  ps )  <->  ( ps  <->  -.  ch )
)
31, 2sylibr 215 1  |-  ( ph  ->  ( ch  <->  -.  ps )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  con1bid  331  r19.9rzv  3836  sotric  4743  sotrieq  4744  sotr2  4746  isso2i  4749  sotri2  5191  sotri3  5192  somin1  5195  somincom  5196  ordtri2  5420  ordintdif  5434  ord0eln0  5439  iotanul  5523  soisoi  6178  weniso  6204  ordunisuc2  6629  limsssuc  6635  nlimon  6636  tfrlem15  7065  oawordeulem  7210  nnawordex  7293  onomeneq  7715  fimaxg  7771  suplub2  7928  fiming  7967  wemapsolem  8018  cantnflem1  8146  rankval3b  8249  cardsdomel  8360  harsdom  8381  isfin1-2  8766  fin1a2lem7  8787  suplem2pr  9429  xrltnle  9652  ltnle  9664  leloe  9671  xrlttri  11389  xrleloe  11394  xrrebnd  11414  supxrbnd2  11559  supxrbnd  11565  om2uzf1oi  12117  rabssnn0fi  12148  cnpart  13247  bits0e  14345  bitsmod  14353  bitsinv1lem  14358  sadcaddlem  14374  trfil2  20844  xrsxmet  21769  metdsge  21808  metdsgeOLD  21823  ovolunlem1a  22391  ovolunlem1  22392  itg2seq  22642  toslublem  28379  tosglblem  28381  isarchi2  28453  gsumesum  28832  sgnneg  29363  nodenselem7  30525  elfuns  30631  finminlem  30923  bj-bibibi  31118  itg2addnclem  31900  heiborlem10  32059  islininds2  39880
  Copyright terms: Public domain W3C validator