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

Theorem con4bid 291
Description: A contraposition deduction. (Contributed by NM, 21-May-1994.)
Hypothesis
Ref Expression
con4bid.1  |-  ( ph  ->  ( -.  ps  <->  -.  ch )
)
Assertion
Ref Expression
con4bid  |-  ( ph  ->  ( ps  <->  ch )
)

Proof of Theorem con4bid
StepHypRef Expression
1 con4bid.1 . . . 4  |-  ( ph  ->  ( -.  ps  <->  -.  ch )
)
21biimprd 223 . . 3  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32con4d 105 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41biimpd 207 . 2  |-  ( ph  ->  ( -.  ps  ->  -. 
ch ) )
53, 4impcon4bid 205 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184
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
This theorem is referenced by:  notbid  292  notbi  293  had0  1479  necon4abidOLD  2634  sbcne12  3753  ordsucuniel  6558  rankr1a  8167  ltaddsub  9944  leaddsub  9946  supxrbnd1  11434  supxrbnd2  11435  ioo0  11475  ico0  11496  ioc0  11497  icc0  11498  fllt  11842  rabssnn0fi  11998  elcls  19660  rusgranumwlks  25077  chrelat3  27406  wl-sb8et  30166  nnolog2flm1  33411
  Copyright terms: Public domain W3C validator