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  871  albi  1610  exbi  1634  cbv2h  1978  equveli  2048  equveliOLD  2049  sbiedOLD  2113  euex  2290  2eu6  2380  2eu6OLD  2381  eleq2d  2524  ceqsalt  3101  euind  3253  reu6  3255  reuind  3270  sbciegft  3325  axpr  4641  iota4  5510  fv3  5815  nn0prpwlem  28685  nn0prpw  28686  tsbi3  29114  axc11next  29828  pm13.192  29832  exbir  31506  con5  31579  sbcim2g  31597  trsspwALT  31904  trsspwALT2  31905  sspwtr  31907  sspwtrALT  31908  pwtrVD  31912  pwtrrVD  31913  snssiALTVD  31915  sstrALT2VD  31922  sstrALT2  31923  suctrALT2VD  31924  eqsbc3rVD  31928  simplbi2VD  31934  exbirVD  31941  exbiriVD  31942  imbi12VD  31961  sbcim2gVD  31963  simplbi2comtVD  31976  con5VD  31988  2uasbanhVD  31999  bj-bi3ant  32467  bj-cbv2hv  32582  bj-ceqsalt0  32736  bj-ceqsalt1  32737  mapdrvallem2  35648
  Copyright terms: Public domain W3C validator