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  3463  elabgtOLD  3616  elabgtOLDOLD  3617  euind  3671  reu6  3673  reuind  3700  sbciegftOLD  3767  replem  5224  sepex  5236  axprALT  5365  axprOLD  5375  iota4  6480  fv3  6859  elirrv  9512  axprALT2  35253  r1omhfb  35256  fineqvpow  35259  r1omhfbregs  35281  nn0prpwlem  36504  nn0prpw  36505  bj-animbi  36823  bj-bi3ant  36854  bj-cbv2hv  37104  bj-ceqsalt0  37191  bj-ceqsalt1  37192  bj-bm1.3ii  37371  bj-axreprepsep  37382  dfgcd3  37638  tsbi3  38456  mapdrvallem2  42091  eu6w  43109  axc11next  44833  pm13.192  44837  exbir  44906  con5  44949  sbcim2g  44965  trsspwALT  45244  trsspwALT2  45245  sspwtr  45247  sspwtrALT  45248  pwtrVD  45250  pwtrrVD  45251  snssiALTVD  45253  sstrALT2VD  45260  sstrALT2  45261  suctrALT2VD  45262  eqsbc2VD  45266  simplbi2VD  45272  exbirVD  45279  exbiriVD  45280  imbi12VD  45299  sbcim2gVD  45301  simplbi2comtVD  45314  con5VD  45326  2uasbanhVD  45337  nimnbi2  45594  absnsb  47469  thincciso  49922