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  necon2abid  2666  necon2bbid  2667  r19.9rzv  3772  sotric  4665  sotrieq  4666  sotr2  4668  isso2i  4671  ordtri2  4752  ordintdif  4766  ord0eln0  4771  sotri2  5225  sotri3  5226  somin1  5232  somincom  5233  iotanul  5394  soisoi  6017  weniso  6043  ordunisuc2  6453  limsssuc  6459  nlimon  6460  tfrlem15  6849  oawordeulem  6991  nnawordex  7074  onomeneq  7498  fimaxg  7557  suplub2  7709  wemapsolem  7762  cantnflem1  7895  cantnflem1OLD  7918  rankval3b  8031  cardsdomel  8142  harsdom  8163  isfin1-2  8552  fin1a2lem7  8573  suplem2pr  9220  xrltnle  9441  ltnle  9452  leloe  9459  xrlttri  11114  xrleloe  11119  xrrebnd  11138  supxrbnd2  11283  supxrbnd  11289  om2uzf1oi  11774  cnpart  12727  bits0e  13623  bitsmod  13630  bitsinv1lem  13635  sadcaddlem  13651  trfil2  19458  xrsxmet  20384  metdsge  20423  ovolunlem1a  20977  ovolunlem1  20978  itg2seq  21218  toslublem  26126  tosglblem  26128  isarchi2  26200  gsumesum  26508  sgnneg  26921  nodenselem7  27826  elfuns  27944  itg2addnclem  28440  finminlem  28510  heiborlem10  28716  rabssnn0fi  30744  islininds2  31015  bj-bibibi  32109
  Copyright terms: Public domain W3C validator