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

Theorem bi2 191
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 186 . 2  |-  ( (
ph 
<->  ps )  <->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
2 simprim 144 . 2  |-  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ps  ->  ph )
)
31, 2sylbi 189 1  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178
This theorem is referenced by:  bicom1  192  pm5.74  237  bi3ant  282  bija  346  pm4.72  851  exbir  1361  simplbi2comg  1369  albi  1552  exbi  1579  cbv2h  1873  sbied  1909  2eu6  2201  ceqsalt  2778  euind  2920  reu6  2922  reuind  2934  sbciegft  2982  axpr  4171  fv3  5460  iota4  6229  wl-bitr1  24271  nn0prpwlem  25591  nn0prpw  25592  ax10ext  26959  pm13.192  26964  astbstanbst  27152  con5  27322  sbcim2g  27339  trsspwALT  27626  trsspwALT2  27627  sspwtr  27629  sspwtrALT  27630  pwtrVD  27632  pwtrrVD  27634  snssiALTVD  27636  sstrALT2VD  27644  sstrALT2  27645  suctrALT2VD  27646  eqsbc3rVD  27650  simplbi2VD  27656  exbirVD  27663  exbiriVD  27664  imbi12VD  27683  sbcim2gVD  27685  simplbi2comgVD  27698  con5VD  27710  2uasbanhVD  27721  mapdrvallem2  30986
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator