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

Theorem biimpr 201
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
Assertion
Ref Expression
biimpr  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )

Proof of Theorem biimpr
StepHypRef Expression
1 dfbi1 194 . 2  |-  ( (
ph 
<->  ps )  <->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
2 simprim 153 . 2  |-  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ps  ->  ph )
)
31, 2sylbi 198 1  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  bicom1  202  pm5.74  247  bija  356  simplbi2comt  630  pm4.72  884  bianir  975  albi  1686  exbi  1711  cbv2h  2073  equveli  2143  euex  2290  2eu6  2356  eleq2d  2492  ceqsalt  3104  euind  3258  reu6  3260  reuind  3275  sbciegft  3330  axpr  4656  iota4  5580  fv3  5891  nn0prpwlem  30971  nn0prpw  30972  bj-bi3ant  31165  bj-cbv2hv  31282  bj-ceqsalt0  31440  bj-ceqsalt1  31441  tsbi3  32291  mapdrvallem2  35132  axc11next  36615  pm13.192  36619  exbir  36691  con5  36737  sbcim2g  36757  trsspwALT  37067  trsspwALT2  37068  sspwtr  37070  sspwtrALT  37071  pwtrVD  37081  pwtrrVD  37082  snssiALTVD  37084  sstrALT2VD  37091  sstrALT2  37092  suctrALT2VD  37093  eqsbc3rVD  37097  simplbi2VD  37103  exbirVD  37110  exbiriVD  37111  imbi12VD  37131  sbcim2gVD  37133  simplbi2comtVD  37146  con5VD  37158  2uasbanhVD  37169
  Copyright terms: Public domain W3C validator