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  1374  simplbi2comg  1382  albi  1573  exbi  1591  cbv2h  1979  equveli  2081  sbiedOLD  2124  2eu6  2365  ceqsalt  2965  euind  3108  reu6  3110  reuind  3124  sbciegft  3178  axpr  4389  iota4  5422  fv3  5730  wl-bitr1  26163  nn0prpwlem  26257  nn0prpw  26258  ax10ext  27516  pm13.192  27520  con5  28359  sbcim2g  28376  trsspwALT  28683  trsspwALT2  28684  sspwtr  28686  sspwtrALT  28687  pwtrVD  28689  pwtrrVD  28690  snssiALTVD  28691  sstrALT2VD  28698  sstrALT2  28699  suctrALT2VD  28700  eqsbc3rVD  28704  simplbi2VD  28710  exbirVD  28717  exbiriVD  28718  imbi12VD  28737  sbcim2gVD  28739  simplbi2comgVD  28752  con5VD  28764  2uasbanhVD  28775  cbv2hwAUX7  29265  sbiedNEW7  29290  cbv2hOLD7  29451  mapdrvallem2  32174
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