Theorem biimpr 222

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 215	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
2		simprim 166	. 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜓 → 𝜑))
3	1, 2	sylbi 219	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

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

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 209

This theorem is referenced by:  bicom1  223  pm5.74  272  bija  382  simplbi2comt  505  pm4.72  962  bianir  1070  albi  1840  spsbbi  2108  cbv2w  2370  cbv2  2436  cbv2h  2439  equvel  2489  dfeumo  2565  eu6  2603  2eu6  2685  ralbi  3119  rexbi  3120  ceqsal1t  3488  elabgtOLD  3634  euind  3689  reu6  3691  reuind  3718  replem  5240  sepex  5252  axprALT  5381  axprOLD  5391  iota4  6504  fv3  6887  elirrvOLD  9548  axprALT2  35409  r1omhfb  35412  fineqvpow  35415  r1omhfbregs  35437  nn0prpwlem  36687  nn0prpw  36688  bj-animbi  37006  bj-bi3ant  37037  bj-cbv2hv  37287  bj-ceqsalt0  37374  bj-ceqsalt1  37375  bj-bm1.3ii  37554  bj-axreprepsep  37565  dfgcd3  37821  tsbi3  38639  mapdrvallem2  42274  eu6w  43263  axc11next  44987  pm13.192  44991  exbir  45060  con5  45103  sbcim2g  45119  trsspwALT  45398  trsspwALT2  45399  sspwtr  45401  sspwtrALT  45402  pwtrVD  45404  pwtrrVD  45405  snssiALTVD  45407  sstrALT2VD  45414  sstrALT2  45415  suctrALT2VD  45416  eqsbc2VD  45420  simplbi2VD  45426  exbirVD  45433  exbiriVD  45434  imbi12VD  45453  sbcim2gVD  45455  simplbi2comtVD  45468  con5VD  45480  2uasbanhVD  45491  nimnbi2  45747  absnsb  47626  thincciso  50079