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

Theorem biimp 196
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.)
Assertion
Ref Expression
biimp  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )

Proof of Theorem biimp
StepHypRef Expression
1 df-bi 188 . . 3  |-  -.  (
( ( ph  <->  ps )  ->  -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph )
) )  ->  -.  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph )
)  ->  ( ph  <->  ps ) ) )
2 simplim 154 . . 3  |-  ( -.  ( ( ( ph  <->  ps )  ->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )  ->  -.  ( -.  ( (
ph  ->  ps )  ->  -.  ( ps  ->  ph )
)  ->  ( ph  <->  ps ) ) )  -> 
( ( ph  <->  ps )  ->  -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph )
) ) )
31, 2ax-mp 5 . 2  |-  ( (
ph 
<->  ps )  ->  -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
4 simplim 154 . 2  |-  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ph  ->  ps )
)
53, 4syl 17 1  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
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:  biimpi  197  bicom1  202  biimpd  210  ibd  246  pm5.74  247  pm5.501  342  bija  356  bianirOLD  976  albi  1684  exbiOLD  1711  cbv2h  2077  mo2v  2276  2eu6  2357  eleq2dOLD  2493  ceqsalt  3104  vtoclgft  3129  spcgft  3158  pm13.183  3211  reu6  3259  reu3  3260  sbciegft  3330  fv3  5894  expeq0  12308  t1t0  20362  kqfvima  20743  ufileu  20932  cvmlift2lem1  30033  btwndiff  30799  nn0prpw  30984  bj-dfbi6  31156  bj-bi3ant  31177  bj-cbv2hv  31294  bj-eumo0  31413  bj-ceqsalt0  31452  bj-ceqsalt1  31453  bj-ax9  31467  bi33imp12  36816  bi23imp1  36821  bi123imp0  36822  eqsbc3rVD  37209  imbi12VD  37243  2uasbanhVD  37281
  Copyright terms: Public domain W3C validator