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  2715  necon2bbidOLD  2717  r19.9rzv  3915  sotric  4819  sotrieq  4820  sotr2  4822  isso2i  4825  ordtri2  4906  ordintdif  4920  ord0eln0  4925  sotri2  5387  sotri3  5388  somin1  5394  somincom  5395  iotanul  5557  soisoi  6203  weniso  6229  ordunisuc2  6650  limsssuc  6656  nlimon  6657  tfrlem15  7051  oawordeulem  7193  nnawordex  7276  onomeneq  7697  fimaxg  7756  suplub2  7910  wemapsolem  7964  cantnflem1  8097  cantnflem1OLD  8120  rankval3b  8233  cardsdomel  8344  harsdom  8365  isfin1-2  8754  fin1a2lem7  8775  suplem2pr  9420  xrltnle  9642  ltnle  9653  leloe  9660  xrlttri  11334  xrleloe  11339  xrrebnd  11358  supxrbnd2  11503  supxrbnd  11509  om2uzf1oi  12020  rabssnn0fi  12051  cnpart  13023  bits0e  13927  bitsmod  13934  bitsinv1lem  13939  sadcaddlem  13955  trfil2  20116  xrsxmet  21042  metdsge  21081  ovolunlem1a  21635  ovolunlem1  21636  itg2seq  21877  toslublem  27303  tosglblem  27305  isarchi2  27377  gsumesum  27693  sgnneg  28105  nodenselem7  29010  elfuns  29128  itg2addnclem  29630  finminlem  29700  heiborlem10  29906  islininds2  32033  bj-bibibi  33131
  Copyright terms: Public domain W3C validator