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

Theorem bi2 189
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 184 . 2  |-  ( (
ph 
<->  ps )  <->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
2 simprim 142 . 2  |-  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ps  ->  ph )
)
31, 2sylbi 187 1  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  bicom1  190  pm5.74  235  bi3ant  280  bija  344  pm4.72  846  exbir  1355  simplbi2comg  1363  albi  1554  exbi  1571  cbv2h  1933  sbied  1989  2eu6  2241  ceqsalt  2823  euind  2965  reu6  2967  reuind  2981  sbciegft  3034  axpr  4229  iota4  5253  fv3  5557  wl-bitr1  24982  nn0prpwlem  26341  nn0prpw  26342  ax10ext  27709  pm13.192  27713  astbstanbst  27980  con5  28584  sbcim2g  28601  trsspwALT  28908  trsspwALT2  28909  sspwtr  28911  sspwtrALT  28912  pwtrVD  28914  pwtrrVD  28916  snssiALTVD  28918  sstrALT2VD  28926  sstrALT2  28927  suctrALT2VD  28928  eqsbc3rVD  28932  simplbi2VD  28938  exbirVD  28945  exbiriVD  28946  imbi12VD  28965  sbcim2gVD  28967  simplbi2comgVD  28980  con5VD  28992  2uasbanhVD  29003  cbv2hwAUX7  29490  sbiedNEW7  29515  cbv2hOLD7  29675  mapdrvallem2  32457
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 177
  Copyright terms: Public domain W3C validator