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  951  bianir  1058  albi  1819  spsbbi  2076  cbv2w  2337  cbv2  2403  cbv2h  2406  equvel  2456  dfeumo  2532  eu6  2569  2eu6  2652  ralbi  3087  rexbi  3088  ceqsal1t  3469  elabgtOLD  3623  elabgtOLDOLD  3624  euind  3678  reu6  3680  reuind  3707  sbciegftOLD  3774  sepex  5236  axprALT  5358  axprOLD  5367  iota4  6462  fv3  6840  elirrv  9483  r1omhfb  35123  r1omhfbregs  35133  fineqvpow  35138  nn0prpwlem  36366  nn0prpw  36367  bj-animbi  36603  bj-bi3ant  36633  bj-cbv2hv  36841  bj-ceqsalt0  36928  bj-ceqsalt1  36929  bj-bm1.3ii  37108  dfgcd3  37368  tsbi3  38174  mapdrvallem2  41743  eu6w  42768  axc11next  44498  pm13.192  44502  exbir  44571  con5  44614  sbcim2g  44630  trsspwALT  44909  trsspwALT2  44910  sspwtr  44912  sspwtrALT  44913  pwtrVD  44915  pwtrrVD  44916  snssiALTVD  44918  sstrALT2VD  44925  sstrALT2  44926  suctrALT2VD  44927  eqsbc2VD  44931  simplbi2VD  44937  exbirVD  44944  exbiriVD  44945  imbi12VD  44964  sbcim2gVD  44966  simplbi2comtVD  44979  con5VD  44991  2uasbanhVD  45002  nimnbi2  45260  absnsb  47126  thincciso  49553