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

Theorem con2bid 329
 Description: A contraposition deduction. (Contributed by NM, 15-Apr-1995.)
Hypothesis
Ref Expression
con2bid.1
Assertion
Ref Expression
con2bid

Proof of Theorem con2bid
StepHypRef Expression
1 con2bid.1 . 2
2 con2bi 328 . 2
31, 2sylibr 212 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4  <->wb 184 This theorem is referenced by:  con1bid  330  necon2abidOLD  2712  necon2bbidOLD  2714  r19.9rzv  3923  sotric  4831  sotrieq  4832  sotr2  4834  isso2i  4837  ordtri2  4918  ordintdif  4932  ord0eln0  4937  sotri2  5401  sotri3  5402  somin1  5408  somincom  5409  iotanul  5571  soisoi  6224  weniso  6250  ordunisuc2  6679  limsssuc  6685  nlimon  6686  tfrlem15  7080  oawordeulem  7222  nnawordex  7305  onomeneq  7727  fimaxg  7787  suplub2  7941  wemapsolem  7996  cantnflem1  8129  cantnflem1OLD  8152  rankval3b  8265  cardsdomel  8376  harsdom  8397  isfin1-2  8786  fin1a2lem7  8807  suplem2pr  9452  xrltnle  9674  ltnle  9685  leloe  9692  xrlttri  11374  xrleloe  11379  xrrebnd  11398  supxrbnd2  11543  supxrbnd  11549  om2uzf1oi  12064  rabssnn0fi  12095  cnpart  13073  bits0e  14079  bitsmod  14086  bitsinv1lem  14091  sadcaddlem  14107  trfil2  20388  xrsxmet  21314  metdsge  21353  ovolunlem1a  21907  ovolunlem1  21908  itg2seq  22149  toslublem  27655  tosglblem  27657  isarchi2  27729  gsumesum  28067  sgnneg  28479  nodenselem7  29447  elfuns  29565  itg2addnclem  30066  finminlem  30136  heiborlem10  30316  islininds2  33085  bj-bibibi  34175 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
 Copyright terms: Public domain W3C validator