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

Theorem con2bid 329
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 328 . 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  330  necon2abidOLD  2698  necon2bbidOLD  2700  r19.9rzv  3909  sotric  4816  sotrieq  4817  sotr2  4819  isso2i  4822  ordtri2  4903  ordintdif  4917  ord0eln0  4922  sotri2  5386  sotri3  5387  somin1  5393  somincom  5394  iotanul  5556  soisoi  6209  weniso  6235  ordunisuc2  6664  limsssuc  6670  nlimon  6671  tfrlem15  7063  oawordeulem  7205  nnawordex  7288  onomeneq  7709  fimaxg  7769  suplub2  7923  wemapsolem  7978  cantnflem1  8111  cantnflem1OLD  8134  rankval3b  8247  cardsdomel  8358  harsdom  8379  isfin1-2  8768  fin1a2lem7  8789  suplem2pr  9434  xrltnle  9656  ltnle  9667  leloe  9674  xrlttri  11356  xrleloe  11361  xrrebnd  11380  supxrbnd2  11525  supxrbnd  11531  om2uzf1oi  12046  rabssnn0fi  12077  cnpart  13055  bits0e  14061  bitsmod  14068  bitsinv1lem  14073  sadcaddlem  14089  trfil2  20366  xrsxmet  21292  metdsge  21331  ovolunlem1a  21885  ovolunlem1  21886  itg2seq  22127  toslublem  27633  tosglblem  27635  isarchi2  27707  gsumesum  28045  sgnneg  28457  nodenselem7  29423  elfuns  29541  itg2addnclem  30042  finminlem  30112  heiborlem10  30292  islininds2  32955  bj-bibibi  34058
  Copyright terms: Public domain W3C validator