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  848  exbir  1357  simplbi2comg  1365  albi  1553  exbi  1570  cbv2h  1925  sbied  1983  2eu6  2231  ceqsalt  2813  euind  2955  reu6  2957  reuind  2971  sbciegft  3024  axpr  4214  fv3  5503  iota4  6272  wl-bitr1  24319  nn0prpwlem  25639  nn0prpw  25640  ax10ext  27007  pm13.192  27011  astbstanbst  27258  con5  27558  sbcim2g  27575  trsspwALT  27862  trsspwALT2  27863  sspwtr  27865  sspwtrALT  27866  pwtrVD  27868  pwtrrVD  27870  snssiALTVD  27872  sstrALT2VD  27880  sstrALT2  27881  suctrALT2VD  27882  eqsbc3rVD  27886  simplbi2VD  27892  exbirVD  27899  exbiriVD  27900  imbi12VD  27919  sbcim2gVD  27921  simplbi2comgVD  27934  con5VD  27946  2uasbanhVD  27957  mapdrvallem2  31104
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