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

Theorem con4bid 286
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 216 . . 3  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32con4d 100 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41biimpd 200 . 2  |-  ( ph  ->  ( -.  ps  ->  -. 
ch ) )
53, 4impcon4bid 198 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178
This theorem is referenced by:  notbid  287  notbi  288  had0  1413  necon4abid  2675  sbcne12  3657  sbcne12gOLD  3658  ordsucuniel  4839  rankr1a  7798  ltaddsub  9540  leaddsub  9542  supxrbnd1  10938  supxrbnd2  10939  ioo0  10979  ico0  11000  ioc0  11001  icc0  11002  fllt  11253  elcls  17175  chrelat3  23912
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 179
  Copyright terms: Public domain W3C validator