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

Theorem con4bid 293
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  294  notbi  295  had0  1446  necon4abidOLD  2700  sbcne12  3777  sbcne12gOLD  3778  ordsucuniel  6535  rankr1a  8144  ltaddsub  9914  leaddsub  9916  supxrbnd1  11385  supxrbnd2  11386  ioo0  11426  ico0  11447  ioc0  11448  icc0  11449  fllt  11757  elcls  18793  chrelat3  25910  wl-sb8et  28515  rusgranumwlks  30712  rabssnn0fi  30885
  Copyright terms: Public domain W3C validator