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  1554  exbi  1571  cbv2h  1933  sbied  1989  eumo0  2180  2eu6  2241  ceqsalt  2823  vtoclgft  2847  spcgft  2873  pm13.183  2921  reu6  2967  reu3  2968  sbciegft  3034  fv3  5557  expeq0  11148  t1t0  17092  kqfvima  17437  ufileu  17630  cvmlift2lem1  23848  btwndiff  24722  wl-bitr1  24982  hdrmp  25809  nn0prpw  26342  atbiffatnnb  27984  bi33imp12  28554  bi23imp13  28555  bi13imp23  28556  bi13imp2  28557  bi12imp3  28558  bi23imp1  28559  bi123imp0  28560  eqsbc3rVD  28932  imbi12VD  28965  2uasbanhVD  29003  bnj926  29115  cbv2hwAUX7  29490  sbiedNEW7  29515  cbv2hOLD7  29675
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