MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bi2 Structured version   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 145 . 2  |-  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ps  ->  ph )
)
31, 2sylbi 189 1  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178
This theorem is referenced by:  bicom1  192  pm5.74  237  bi3ant  282  bija  346  pm4.72  848  exbir  1375  simplbi2comg  1383  albi  1574  exbi  1592  cbv2h  1982  equveli  2088  sbiedOLD  2157  2eu6  2372  ceqsalt  2984  euind  3127  reu6  3129  reuind  3143  sbciegft  3197  axpr  4431  iota4  5465  fv3  5773  wl-bitr1  26251  nn0prpwlem  26363  nn0prpw  26364  ax10ext  27621  pm13.192  27625  con5  28704  sbcim2g  28721  trsspwALT  29029  trsspwALT2  29030  sspwtr  29032  sspwtrALT  29033  pwtrVD  29035  pwtrrVD  29036  snssiALTVD  29037  sstrALT2VD  29044  sstrALT2  29045  suctrALT2VD  29046  eqsbc3rVD  29050  simplbi2VD  29056  exbirVD  29063  exbiriVD  29064  imbi12VD  29083  sbcim2gVD  29085  simplbi2comgVD  29098  con5VD  29110  2uasbanhVD  29121  cbv2hwAUX7  29611  sbiedNEW7  29638  cbv2hOLD7  29819  mapdrvallem2  32541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator