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

Theorem biimpr 202
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 195 . 2  |-  ( (
ph 
<->  ps )  <->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
2 simprim 154 . 2  |-  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ps  ->  ph )
)
31, 2sylbi 199 1  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  bicom1  203  pm5.74  248  bija  357  simplbi2comt  632  pm4.72  888  bianir  979  albi  1692  exbiOLD  1719  cbv2h  2114  equveli  2182  euex  2325  2eu6  2389  eleq2dOLD  2517  ceqsalt  3072  euind  3227  reu6  3229  reuind  3245  sbciegft  3300  axpr  4641  iota4  5567  fv3  5883  nn0prpwlem  30990  nn0prpw  30991  bj-bi3ant  31185  bj-ssbbi  31247  bj-cbv2hv  31344  bj-ceqsalt0  31494  bj-ceqsalt1  31495  tsbi3  32389  mapdrvallem2  35225  axc11next  36768  pm13.192  36772  exbir  36844  con5  36890  sbcim2g  36910  trsspwALT  37216  trsspwALT2  37217  sspwtr  37219  sspwtrALT  37220  pwtrVD  37230  pwtrrVD  37231  snssiALTVD  37233  sstrALT2VD  37240  sstrALT2  37241  suctrALT2VD  37242  eqsbc3rVD  37246  simplbi2VD  37252  exbirVD  37259  exbiriVD  37260  imbi12VD  37280  sbcim2gVD  37282  simplbi2comtVD  37295  con5VD  37307  2uasbanhVD  37318
  Copyright terms: Public domain W3C validator