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

Theorem bi2 198
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
Assertion
Ref Expression
bi2  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )

Proof of Theorem bi2
StepHypRef Expression
1 dfbi1 192 . 2  |-  ( (
ph 
<->  ps )  <->  -.  (
( ph  ->  ps )  ->  -.  ( ps  ->  ph ) ) )
2 simprim 150 . 2  |-  ( -.  ( ( ph  ->  ps )  ->  -.  ( ps  ->  ph ) )  -> 
( ps  ->  ph )
)
31, 2sylbi 195 1  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
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:  bicom1  199  pm5.74  244  bi3antOLD  289  bija  355  simplbi2comt  626  pm4.72  874  albi  1619  exbi  1643  cbv2h  1991  equveli  2061  equveliOLD  2062  sbiedOLD  2126  euex  2303  2eu6  2393  2eu6OLD  2394  eleq2d  2537  ceqsalt  3136  euind  3290  reu6  3292  reuind  3307  sbciegft  3362  axpr  4685  iota4  5569  fv3  5879  nn0prpwlem  29993  nn0prpw  29994  tsbi3  30373  axc11next  31118  pm13.192  31122  exbir  32515  con5  32588  sbcim2g  32606  trsspwALT  32913  trsspwALT2  32914  sspwtr  32916  sspwtrALT  32917  pwtrVD  32921  pwtrrVD  32922  snssiALTVD  32924  sstrALT2VD  32931  sstrALT2  32932  suctrALT2VD  32933  eqsbc3rVD  32937  simplbi2VD  32943  exbirVD  32950  exbiriVD  32951  imbi12VD  32970  sbcim2gVD  32972  simplbi2comtVD  32985  con5VD  32997  2uasbanhVD  33008  bj-bi3ant  33476  bj-cbv2hv  33593  bj-ceqsalt0  33747  bj-ceqsalt1  33748  mapdrvallem2  36659  bj-frege52a  37085
  Copyright terms: Public domain W3C validator