Theorem biimpr 210

Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)

Assertion

Ref	Expression
biimpr	|- ( ( ph <-> ps ) -> ( ps -> ph ) )

Proof of Theorem biimpr

Step	Hyp	Ref	Expression
1		dfbi1 203	. 2 |- ( ( ph <-> ps ) <-> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) )
2		simprim 162	. 2 |- ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> ( ps -> ph ) )
3	1, 2	sylbi 207	1 |- ( ( ph <-> ps ) -> ( ps -> ph ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  bicom1  211  pm5.74  259  bija  370  simplbi2comt  656  pm4.72  920  bianir  1009  albi  1746  cbv2h  2269  equvel  2347  euex  2494  2eu6  2558  ceqsalt  3228  euind  3393  reu6  3395  reuind  3411  sbciegft  3466  axpr  4905  iota4  5869  fv3  6206  nn0prpwlem  32317  nn0prpw  32318  bj-bi3ant  32574  bj-ssbbi  32622  bj-cbv2hv  32731  bj-ceqsalt0  32873  bj-ceqsalt1  32874  dfgcd3  33170  tsbi3  33942  mapdrvallem2  36934  axc11next  38607  pm13.192  38611  exbir  38684  con5  38728  sbcim2g  38748  trsspwALT  39045  trsspwALT2  39046  sspwtr  39048  sspwtrALT  39049  pwtrVD  39059  pwtrrVD  39060  snssiALTVD  39062  sstrALT2VD  39069  sstrALT2  39070  suctrALT2VD  39071  eqsbc3rVD  39075  simplbi2VD  39081  exbirVD  39088  exbiriVD  39089  imbi12VD  39109  sbcim2gVD  39111  simplbi2comtVD  39124  con5VD  39136  2uasbanhVD  39147