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

Theorem con4bid 294
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 226 . . 3  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32con4d 108 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41biimpd 210 . 2  |-  ( ph  ->  ( -.  ps  ->  -. 
ch ) )
53, 4impcon4bid 208 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  notbid  295  notbi  296  had0  1502  necon4abidOLD  2676  sbcne12  3803  ordsucuniel  6661  rankr1a  8308  ltaddsub  10088  leaddsub  10090  supxrbnd1  11607  supxrbnd2  11608  ioo0  11661  ico0  11682  ioc0  11683  icc0  11684  fllt  12041  rabssnn0fi  12197  elcls  20075  rusgranumwlks  25669  chrelat3  28009  wl-sb8et  31794  nnolog2flm1  39674
  Copyright terms: Public domain W3C validator