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  2015  sbied  2069  2eu6  2323  ceqsalt  2921  euind  3064  reu6  3066  reuind  3080  sbciegft  3134  axpr  4343  iota4  5376  fv3  5684  wl-bitr1  25934  nn0prpwlem  26016  nn0prpw  26017  ax10ext  27275  pm13.192  27279  con5  27949  sbcim2g  27966  trsspwALT  28272  trsspwALT2  28273  sspwtr  28275  sspwtrALT  28276  pwtrVD  28278  pwtrrVD  28279  snssiALTVD  28280  sstrALT2VD  28287  sstrALT2  28288  suctrALT2VD  28289  eqsbc3rVD  28293  simplbi2VD  28299  exbirVD  28306  exbiriVD  28307  imbi12VD  28326  sbcim2gVD  28328  simplbi2comgVD  28341  con5VD  28353  2uasbanhVD  28364  cbv2hwAUX7  28851  sbiedNEW7  28876  cbv2hOLD7  29037  mapdrvallem2  31760
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