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

Theorem con4bid 284
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 214 . . 3  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32con4d 97 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41biimpd 198 . 2  |-  ( ph  ->  ( -.  ps  ->  -. 
ch ) )
53, 4impcon4bid 196 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  notbid  285  notbi  286  had0  1403  necon4abid  2585  sbcne12g  3175  ordsucuniel  4697  rankr1a  7598  ltaddsub  9338  leaddsub  9340  supxrbnd1  10732  supxrbnd2  10733  ioo0  10773  ico0  10794  ioc0  10795  icc0  10796  fllt  11030  elcls  16916  chrelat3  23065  isoun  23293
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 177
  Copyright terms: Public domain W3C validator