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

Theorem biimpr 203
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
Assertion
Ref Expression
biimpr  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )

Proof of Theorem biimpr
StepHypRef Expression
1 dfbi1 196 . 2  |-  ( (
ph 
<->  ps )  <->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
2 simprim 155 . 2  |-  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ps  ->  ph )
)
31, 2sylbi 200 1  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  bicom1  204  pm5.74  252  bija  362  simplbi2comt  638  pm4.72  893  bianir  978  albi  1698  exbiOLD  1725  cbv2h  2125  equveli  2196  euex  2343  2eu6  2407  eleq2dOLD  2535  ceqsalt  3056  euind  3213  reu6  3215  reuind  3231  sbciegft  3286  axpr  4638  iota4  5571  fv3  5892  nn0prpwlem  31049  nn0prpw  31050  bj-bi3ant  31237  bj-ssbbi  31299  bj-cbv2hv  31398  bj-ceqsalt0  31550  bj-ceqsalt1  31551  tsbi3  32441  mapdrvallem2  35284  axc11next  36827  pm13.192  36831  exbir  36903  con5  36949  sbcim2g  36969  trsspwALT  37269  trsspwALT2  37270  sspwtr  37272  sspwtrALT  37273  pwtrVD  37283  pwtrrVD  37284  snssiALTVD  37286  sstrALT2VD  37293  sstrALT2  37294  suctrALT2VD  37295  eqsbc3rVD  37299  simplbi2VD  37305  exbirVD  37312  exbiriVD  37313  imbi12VD  37333  sbcim2gVD  37335  simplbi2comtVD  37348  con5VD  37360  2uasbanhVD  37371
  Copyright terms: Public domain W3C validator