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

Theorem bi1 180
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 179 . . 3  |-  -.  (
( ( ph  <->  ps )  ->  -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph )
) )  ->  -.  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph )
)  ->  ( ph  <->  ps ) ) )
2 simplim 146 . . 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 146 . 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 178
This theorem is referenced by:  biimpi  188  bicom1  192  biimpd  200  ibd  236  pm5.74  237  bi3ant  282  pm5.501  332  bija  346  albi  1574  exbi  1592  cbv2h  1980  equveli  2086  sbied  2151  eumo0  2307  2eu6  2368  ceqsalt  2980  vtoclgft  3004  spcgft  3030  pm13.183  3078  reu6  3125  reu3  3126  sbciegft  3193  fv3  5747  expeq0  11415  t1t0  17417  kqfvima  17767  ufileu  17956  cvmlift2lem1  24994  btwndiff  25966  wl-bitr1  26225  nn0prpw  26339  bi33imp12  28646  bi23imp1  28651  bi123imp0  28652  eqsbc3rVD  29025  imbi12VD  29058  2uasbanhVD  29096  bnj926  29211  cbv2hwAUX7  29586  sbiedNEW7  29613  cbv2hOLD7  29794
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 179
  Copyright terms: Public domain W3C validator