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

Theorem con1bid 330
Description: A contraposition deduction. (Contributed by NM, 9-Oct-1999.)
Hypothesis
Ref Expression
con1bid.1
Assertion
Ref Expression
con1bid

Proof of Theorem con1bid
StepHypRef Expression
1 con1bid.1 . . . 4
21bicomd 201 . . 3
32con2bid 329 . 2
43bicomd 201 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184
This theorem is referenced by:  pm5.18  356  necon1abidOLD  2706  necon1bbid  2707  onmindif  4972  ondif2  7171  cnpart  13073  sadadd2lem2  14100  isnirred  17349  isreg2  19878  kqcldsat  20234  trufil  20411  itg2cnlem2  22169  issqf  23410  eupath2lem3  24979  pjnorm2  26645  atdmd  27317  atmd2  27319  dfrdg4  29600  dalawlem13  35607
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