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

Theorem con2bid 319
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 318 . 2  |-  ( ( ch  <->  -.  ps )  <->  ( ps  <->  -.  ch )
)
31, 2sylibr 203 1  |-  ( ph  ->  ( ch  <->  -.  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  con1bid  320  necon2abid  2516  necon2bbid  2517  r19.9rzv  3561  sotric  4356  sotrieq  4357  sotr2  4359  isso2i  4362  ordtri2  4443  ordintdif  4457  ord0eln0  4462  ordunisuc2  4651  limsssuc  4657  nlimon  4658  sotri2  5088  sotri3  5089  somin1  5095  somincom  5096  iotanul  5250  soisoi  5841  weniso  5868  tfrlem15  6424  oawordeulem  6568  nnawordex  6651  onomeneq  7066  fimaxg  7120  suplub2  7228  wemapso2lem  7281  cantnflem1  7407  rankval3b  7514  cardsdomel  7623  harsdom  7644  isfin1-2  8027  fin1a2lem7  8048  suplem2pr  8693  xrltnle  8907  ltnle  8918  leloe  8924  xrlttri  10489  xrleloe  10494  xrrebnd  10513  supxrbnd2  10657  supxrbnd  10663  om2uzf1oi  11032  cnpart  11741  bits0e  12636  bitsmod  12643  bitsinv1lem  12648  sadcaddlem  12664  trfil2  17598  xrsxmet  18331  metdsge  18369  ovolunlem1a  18871  ovolunlem1  18872  itg2seq  19113  nodenselem7  24412  finminlem  26334  heiborlem10  26647  stoweidlem34  27886
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator