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

Theorem con2bid 327
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 326 . 2  |-  ( ( ch  <->  -.  ps )  <->  ( ps  <->  -.  ch )
)
31, 2sylibr 212 1  |-  ( ph  ->  ( ch  <->  -.  ps )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  con1bid  328  necon2abidOLD  2637  necon2bbidOLD  2639  r19.9rzv  3839  sotric  4740  sotrieq  4741  sotr2  4743  isso2i  4746  ordtri2  4827  ordintdif  4841  ord0eln0  4846  sotri2  5309  sotri3  5310  somin1  5313  somincom  5314  iotanul  5475  soisoi  6125  weniso  6151  ordunisuc2  6578  limsssuc  6584  nlimon  6585  tfrlem15  6979  oawordeulem  7121  nnawordex  7204  onomeneq  7626  fimaxg  7682  suplub2  7835  wemapsolem  7890  cantnflem1  8021  cantnflem1OLD  8044  rankval3b  8157  cardsdomel  8268  harsdom  8289  isfin1-2  8678  fin1a2lem7  8699  suplem2pr  9342  xrltnle  9564  ltnle  9575  leloe  9582  xrlttri  11266  xrleloe  11271  xrrebnd  11290  supxrbnd2  11435  supxrbnd  11441  om2uzf1oi  11967  rabssnn0fi  11998  cnpart  13075  bits0e  14081  bitsmod  14088  bitsinv1lem  14093  sadcaddlem  14109  trfil2  20473  xrsxmet  21399  metdsge  21438  ovolunlem1a  21992  ovolunlem1  21993  itg2seq  22234  toslublem  27808  tosglblem  27810  isarchi2  27882  gsumesum  28207  sgnneg  28662  nodenselem7  29612  elfuns  29718  itg2addnclem  30232  finminlem  30302  heiborlem10  30482  islininds2  33285  bj-bibibi  34522
  Copyright terms: Public domain W3C validator