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

Theorem bi2 190
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 185 . 2  |-  ( (
ph 
<->  ps )  <->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
2 simprim 144 . 2  |-  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ps  ->  ph )
)
31, 2sylbi 188 1  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  bicom1  191  pm5.74  236  bi3ant  281  bija  345  pm4.72  847  exbir  1371  simplbi2comg  1379  albi  1570  exbi  1588  cbv2h  2033  equveli  2042  sbied  2085  2eu6  2339  ceqsalt  2938  euind  3081  reu6  3083  reuind  3097  sbciegft  3151  axpr  4362  iota4  5395  fv3  5703  wl-bitr1  26124  nn0prpwlem  26215  nn0prpw  26216  ax10ext  27474  pm13.192  27478  con5  28317  sbcim2g  28334  trsspwALT  28640  trsspwALT2  28641  sspwtr  28643  sspwtrALT  28644  pwtrVD  28646  pwtrrVD  28647  snssiALTVD  28648  sstrALT2VD  28655  sstrALT2  28656  suctrALT2VD  28657  eqsbc3rVD  28661  simplbi2VD  28667  exbirVD  28674  exbiriVD  28675  imbi12VD  28694  sbcim2gVD  28696  simplbi2comgVD  28709  con5VD  28721  2uasbanhVD  28732  cbv2hwAUX7  29219  sbiedNEW7  29244  cbv2hOLD7  29405  mapdrvallem2  32128
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 178
  Copyright terms: Public domain W3C validator