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  3093  rexbi  3094  ceqsal1t  3475  elabgtOLD  3629  elabgtOLDOLD  3630  euind  3684  reu6  3686  reuind  3713  sbciegftOLD  3780  replem  5237  sepex  5249  axprALT  5371  axprOLD  5380  iota4  6483  fv3  6862  elirrv  9516  axprALT2  35293  r1omhfb  35296  fineqvpow  35299  r1omhfbregs  35321  nn0prpwlem  36544  nn0prpw  36545  bj-animbi  36791  bj-bi3ant  36822  bj-cbv2hv  37072  bj-ceqsalt0  37159  bj-ceqsalt1  37160  bj-bm1.3ii  37339  bj-axreprepsep  37350  dfgcd3  37606  tsbi3  38415  mapdrvallem2  42050  eu6w  43063  axc11next  44791  pm13.192  44795  exbir  44864  con5  44907  sbcim2g  44923  trsspwALT  45202  trsspwALT2  45203  sspwtr  45205  sspwtrALT  45206  pwtrVD  45208  pwtrrVD  45209  snssiALTVD  45211  sstrALT2VD  45218  sstrALT2  45219  suctrALT2VD  45220  eqsbc2VD  45224  simplbi2VD  45230  exbirVD  45237  exbiriVD  45238  imbi12VD  45257  sbcim2gVD  45259  simplbi2comtVD  45272  con5VD  45284  2uasbanhVD  45295  nimnbi2  45552  absnsb  47416  thincciso  49841