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

Theorem bi1 186
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 185 . . 3  |-  -.  (
( ( ph  <->  ps )  ->  -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph )
) )  ->  -.  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph )
)  ->  ( ph  <->  ps ) ) )
2 simplim 151 . . 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 151 . 2  |-  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ph  ->  ps )
)
53, 4syl 16 1  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  biimpi  194  bicom1  199  biimpd  207  ibd  243  pm5.74  244  bi3antOLD  289  pm5.501  341  bija  355  bianir  965  albi  1619  exbi  1643  cbv2h  1991  equveliOLD  2062  sbiedOLD  2126  mo2v  2282  mo2vOLD  2283  mo2vOLDOLD  2284  eumo0OLD  2313  2eu6  2393  2eu6OLD  2394  eleq2d  2537  ceqsalt  3141  vtoclgft  3166  spcgft  3195  pm13.183  3249  reu6  3297  reu3  3298  sbciegft  3367  fv3  5885  expeq0  12176  t1t0  19717  kqfvima  20099  ufileu  20288  cvmlift2lem1  28572  btwndiff  29604  nn0prpw  30068  bi33imp12  32739  bi23imp1  32744  bi123imp0  32745  eqsbc3rVD  33121  imbi12VD  33154  2uasbanhVD  33192  bj-dfbi6  33624  bj-bi3ant  33660  bj-cbv2hv  33777  bj-eumo0  33896  bj-ceqsalt0  33931  bj-ceqsalt1  33932  bj-ax9  33946  frege52aid  37268  bj-frege52a  37269
  Copyright terms: Public domain W3C validator