Theorem biimpr 209

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 202	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
2		simprim 161	. 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜓 → 𝜑))
3	1, 2	sylbi 206	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

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

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 196

This theorem is referenced by:  bicom1  210  pm5.74  258  bija  369  simplbi2comt  654  pm4.72  916  bianir  1001  albi  1736  exbiOLD  1763  cbv2h  2257  equvel  2335  euex  2482  2eu6  2546  eleq2dOLD  2674  ceqsalt  3201  euind  3360  reu6  3362  reuind  3378  sbciegft  3433  axpr  4832  iota4  5786  fv3  6116  nn0prpwlem  31487  nn0prpw  31488  bj-bi3ant  31747  bj-ssbbi  31811  bj-cbv2hv  31918  bj-ceqsalt0  32067  bj-ceqsalt1  32068  tsbi3  33112  mapdrvallem2  35952  axc11next  37629  pm13.192  37633  exbir  37705  con5  37749  sbcim2g  37769  trsspwALT  38067  trsspwALT2  38068  sspwtr  38070  sspwtrALT  38071  pwtrVD  38081  pwtrrVD  38082  snssiALTVD  38084  sstrALT2VD  38091  sstrALT2  38092  suctrALT2VD  38093  eqsbc3rVD  38097  simplbi2VD  38103  exbirVD  38110  exbiriVD  38111  imbi12VD  38131  sbcim2gVD  38133  simplbi2comtVD  38146  con5VD  38158  2uasbanhVD  38169