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

Theorem biimp 198
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 190 . . 3  |-  -.  (
( ( ph  <->  ps )  ->  -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph )
) )  ->  -.  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph )
)  ->  ( ph  <->  ps ) ) )
2 simplim 156 . . 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 156 . 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 189
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 190
This theorem is referenced by:  biimpi  199  bicom1  204  biimpd  212  ibd  251  pm5.74  252  pm5.501  347  bija  361  bianirOLD  985  albi  1701  exbiOLD  1728  cbv2h  2123  mo2v  2317  2eu6  2398  eleq2dOLD  2526  ceqsalt  3082  vtoclgft  3108  spcgft  3138  pm13.183  3191  reu6  3239  reu3  3240  sbciegft  3310  fv3  5901  expeq0  12334  t1t0  20413  kqfvima  20794  ufileu  20983  cvmlift2lem1  30074  btwndiff  30843  nn0prpw  31028  bj-dfbi6  31196  bj-bi3ant  31218  bj-ssbbi  31280  bj-cbv2hv  31377  bj-eumo0  31488  bj-ceqsalt0  31527  bj-ceqsalt1  31528  bj-ax9  31543  bi33imp12  36890  bi23imp1  36895  bi123imp0  36896  eqsbc3rVD  37276  imbi12VD  37310  2uasbanhVD  37348
  Copyright terms: Public domain W3C validator