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

Theorem con4bid 285
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 215 . . 3  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32con4d 99 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41biimpd 199 . 2  |-  ( ph  ->  ( -.  ps  ->  -. 
ch ) )
53, 4impcon4bid 197 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  notbid  286  notbi  287  had0  1409  necon4abid  2639  sbcne12g  3237  ordsucuniel  4771  rankr1a  7726  ltaddsub  9466  leaddsub  9468  supxrbnd1  10864  supxrbnd2  10865  ioo0  10905  ico0  10926  ioc0  10927  icc0  10928  fllt  11178  elcls  17100  chrelat3  23835
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator