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  bija  353  simplbi2comt  624  pm4.72  874  albi  1644  exbi  1671  cbv2h  2024  equveli  2092  euex  2310  2eu6  2380  2eu6OLD  2381  eleq2d  2524  ceqsalt  3129  euind  3283  reu6  3285  reuind  3300  sbciegft  3355  axpr  4675  iota4  5552  fv3  5861  nn0prpwlem  30383  nn0prpw  30384  tsbi3  30785  axc11next  31557  pm13.192  31561  exbir  33625  con5  33698  sbcim2g  33718  trsspwALT  34029  trsspwALT2  34030  sspwtr  34032  sspwtrALT  34033  pwtrVD  34043  pwtrrVD  34044  snssiALTVD  34046  sstrALT2VD  34053  sstrALT2  34054  suctrALT2VD  34055  eqsbc3rVD  34059  simplbi2VD  34065  exbirVD  34072  exbiriVD  34073  imbi12VD  34093  sbcim2gVD  34095  simplbi2comtVD  34108  con5VD  34120  2uasbanhVD  34131  bj-bi3ant  34598  bj-cbv2hv  34714  bj-ceqsalt0  34869  bj-ceqsalt1  34870  mapdrvallem2  37788
  Copyright terms: Public domain W3C validator