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

Step	Hyp	Ref	Expression
1		con2bid.1	. 2
2		con2bi 328	. 2
3	1, 2	sylibr 212	1

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