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

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

Proof of Theorem bi1
StepHypRef Expression
1 df-bi 178 . . 3  |-  -.  (
( ( ph  <->  ps )  ->  -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph )
) )  ->  -.  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph )
)  ->  ( ph  <->  ps ) ) )
2 simplim 145 . . 3  |-  ( -.  ( ( ( ph  <->  ps )  ->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )  ->  -.  ( -.  ( (
ph  ->  ps )  ->  -.  ( ps  ->  ph )
)  ->  ( ph  <->  ps ) ) )  -> 
( ( ph  <->  ps )  ->  -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph )
) ) )
31, 2ax-mp 8 . 2  |-  ( (
ph 
<->  ps )  ->  -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
4 simplim 145 . 2  |-  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ph  ->  ps )
)
53, 4syl 16 1  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  biimpi  187  bicom1  191  biimpd  199  ibd  235  pm5.74  236  bi3ant  281  pm5.501  331  bija  345  albi  1570  exbi  1588  equveli  2044  cbv2h  2054  sbied  2093  eumo0  2286  2eu6  2347  ceqsalt  2946  vtoclgft  2970  spcgft  2996  pm13.183  3044  reu6  3091  reu3  3092  sbciegft  3159  fv3  5711  expeq0  11373  t1t0  17374  kqfvima  17723  ufileu  17912  cvmlift2lem1  24950  btwndiff  25873  wl-bitr1  26132  nn0prpw  26224  bi33imp12  28295  bi23imp1  28300  bi123imp0  28301  eqsbc3rVD  28670  imbi12VD  28703  2uasbanhVD  28741  bnj926  28856  cbv2hwAUX7  29231  sbiedNEW7  29256  cbv2hOLD7  29417
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator