Theorem biimpr 220

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

Assertion

Ref	Expression
biimpr	⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

Proof of Theorem biimpr

Step	Hyp	Ref	Expression
1		dfbi1 213	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
2		simprim 166	. 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜓 → 𝜑))
3	1, 2	sylbi 217	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bicom1  221  pm5.74  270  bija  380  simplbi2comt  501  pm4.72  952  bianir  1059  albi  1820  spsbbi  2079  cbv2w  2342  cbv2  2408  cbv2h  2411  equvel  2461  dfeumo  2537  eu6  2575  2eu6  2658  ralbi  3092  rexbi  3093  ceqsal1t  3474  elabgtOLD  3628  elabgtOLDOLD  3629  euind  3683  reu6  3685  reuind  3712  sbciegftOLD  3779  sepex  5246  axprALT  5368  axprOLD  5377  iota4  6474  fv3  6853  elirrv  9506  r1omhfb  35270  fineqvpow  35273  r1omhfbregs  35295  nn0prpwlem  36518  nn0prpw  36519  bj-animbi  36761  bj-bi3ant  36791  bj-cbv2hv  37000  bj-ceqsalt0  37087  bj-ceqsalt1  37088  bj-bm1.3ii  37267  dfgcd3  37531  tsbi3  38338  mapdrvallem2  41973  eu6w  42986  axc11next  44714  pm13.192  44718  exbir  44787  con5  44830  sbcim2g  44846  trsspwALT  45125  trsspwALT2  45126  sspwtr  45128  sspwtrALT  45129  pwtrVD  45131  pwtrrVD  45132  snssiALTVD  45134  sstrALT2VD  45141  sstrALT2  45142  suctrALT2VD  45143  eqsbc2VD  45147  simplbi2VD  45153  exbirVD  45160  exbiriVD  45161  imbi12VD  45180  sbcim2gVD  45182  simplbi2comtVD  45195  con5VD  45207  2uasbanhVD  45218  nimnbi2  45475  absnsb  47340  thincciso  49765