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  1872  sbied  1908  2eu6  2198  ceqsalt  2748  euind  2889  reu6  2893  reuind  2903  sbciegft  2951  axpr  4107  fv3  5393  iota4  6161  wl-bitr1  24084  nn0prpwlem  25404  nn0prpw  25405  ax10ext  26772  pm13.192  26777  con5  26978  sbcim2g  26995  trsspwALT  27282  trsspwALT2  27283  sspwtr  27285  sspwtrALT  27286  pwtrVD  27288  pwtrrVD  27290  snssiALTVD  27292  sstrALT2VD  27300  sstrALT2  27301  suctrALT2VD  27302  eqsbc3rVD  27306  simplbi2VD  27312  exbirVD  27319  exbiriVD  27320  imbi12VD  27339  sbcim2gVD  27341  simplbi2comgVD  27354  con5VD  27366  2uasbanhVD  27377  mapdrvallem2  30524
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