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

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

Proof of Theorem bi2
StepHypRef Expression
1 dfbi1 184 . 2  |-  ( (
ph 
<->  ps )  <->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
2 simprim 142 . 2  |-  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ps  ->  ph )
)
31, 2sylbi 187 1  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  bicom1  190  pm5.74  235  bi3ant  280  bija  344  pm4.72  846  exbir  1355  simplbi2comg  1363  albi  1551  exbi  1568  cbv2h  1920  sbied  1976  2eu6  2228  ceqsalt  2810  euind  2952  reu6  2954  reuind  2968  sbciegft  3021  axpr  4213  iota4  5237  fv3  5541  wl-bitr1  24910  nn0prpwlem  26238  nn0prpw  26239  ax10ext  27606  pm13.192  27610  astbstanbst  27877  con5  28285  sbcim2g  28302  trsspwALT  28592  trsspwALT2  28593  sspwtr  28595  sspwtrALT  28596  pwtrVD  28598  pwtrrVD  28600  snssiALTVD  28602  sstrALT2VD  28610  sstrALT2  28611  suctrALT2VD  28612  eqsbc3rVD  28616  simplbi2VD  28622  exbirVD  28629  exbiriVD  28630  imbi12VD  28649  sbcim2gVD  28651  simplbi2comgVD  28664  con5VD  28676  2uasbanhVD  28687  mapdrvallem2  31835
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