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  1393  necon4abid  2510  sbcne12g  3099  ordsucuniel  4615  rankr1a  7508  ltaddsub  9248  leaddsub  9250  supxrbnd1  10640  supxrbnd2  10641  ioo0  10681  ico0  10702  ioc0  10703  icc0  10704  fllt  10938  elcls  16810  chrelat3  22951  isoun  23242
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