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  2341  cbv2  2407  cbv2h  2410  equvel  2460  dfeumo  2536  eu6  2574  2eu6  2657  ralbi  3092  rexbi  3093  ceqsal1t  3462  elabgtOLD  3615  elabgtOLDOLD  3616  euind  3670  reu6  3672  reuind  3699  sbciegftOLD  3766  replem  5223  sepex  5235  axprALT  5364  axprOLD  5374  iota4  6479  fv3  6858  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  47475  thincciso  49928