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

Theorem con4bid 293
Description: A contraposition deduction. (Contributed by NM, 21-May-1994.)
Hypothesis
Ref Expression
con4bid.1
Assertion
Ref Expression
con4bid

Proof of Theorem con4bid
StepHypRef Expression
1 con4bid.1 . . . 4
21biimprd 223 . . 3
32con4d 105 . 2
41biimpd 207 . 2
53, 4impcon4bid 205 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184
This theorem is referenced by:  notbid  294  notbi  295  had0  1471  necon4abidOLD  2709  sbcne12  3827  sbcne12gOLD  3828  ordsucuniel  6659  rankr1a  8275  ltaddsub  10051  leaddsub  10053  supxrbnd1  11542  supxrbnd2  11543  ioo0  11583  ico0  11604  ioc0  11605  icc0  11606  fllt  11943  rabssnn0fi  12095  elcls  19574  rusgranumwlks  24956  chrelat3  27290  wl-sb8et  30001
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