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  1873  sbied  1909  2eu6  2201  ceqsalt  2761  euind  2903  reu6  2907  reuind  2917  sbciegft  2965  axpr  4151  fv3  5439  iota4  6208  wl-bitr1  24250  nn0prpwlem  25570  nn0prpw  25571  ax10ext  26938  pm13.192  26943  astbstanbst  27131  con5  27301  sbcim2g  27318  trsspwALT  27605  trsspwALT2  27606  sspwtr  27608  sspwtrALT  27609  pwtrVD  27611  pwtrrVD  27613  snssiALTVD  27615  sstrALT2VD  27623  sstrALT2  27624  suctrALT2VD  27625  eqsbc3rVD  27629  simplbi2VD  27635  exbirVD  27642  exbiriVD  27643  imbi12VD  27662  sbcim2gVD  27664  simplbi2comgVD  27677  con5VD  27689  2uasbanhVD  27700  mapdrvallem2  30965
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