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

Theorem bi1 178
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 177 . . 3  |-  -.  (
( ( ph  <->  ps )  ->  -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph )
) )  ->  -.  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph )
)  ->  ( ph  <->  ps ) ) )
2 simplim 143 . . 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 143 . 2  |-  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ph  ->  ps )
)
53, 4syl 15 1  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  biimpi  186  bicom1  190  biimpd  198  ibd  234  pm5.74  235  bi3ant  280  pm5.501  330  bija  344  albi  1551  exbi  1568  cbv2h  1920  sbied  1976  eumo0  2167  2eu6  2228  ceqsalt  2810  vtoclgft  2834  spcgft  2860  pm13.183  2908  reu6  2954  reu3  2955  sbciegft  3021  fv3  5541  expeq0  11132  t1t0  17076  kqfvima  17421  ufileu  17614  cvmlift2lem1  23833  btwndiff  24650  wl-bitr1  24910  hdrmp  25706  nn0prpw  26239  atbiffatnnb  27881  eqsbc3rVD  28616  imbi12VD  28649  2uasbanhVD  28687  bnj926  28799
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 177
  Copyright terms: Public domain W3C validator