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  5361  axprOLD  5371  iota4  6475  fv3  6854  elirrv  9507  axprALT2  35273  r1omhfb  35276  fineqvpow  35279  r1omhfbregs  35301  nn0prpwlem  36524  nn0prpw  36525  bj-animbi  36843  bj-bi3ant  36874  bj-cbv2hv  37124  bj-ceqsalt0  37211  bj-ceqsalt1  37212  bj-bm1.3ii  37391  bj-axreprepsep  37402  dfgcd3  37658  tsbi3  38474  mapdrvallem2  42109  eu6w  43127  axc11next  44855  pm13.192  44859  exbir  44928  con5  44971  sbcim2g  44987  trsspwALT  45266  trsspwALT2  45267  sspwtr  45269  sspwtrALT  45270  pwtrVD  45272  pwtrrVD  45273  snssiALTVD  45275  sstrALT2VD  45282  sstrALT2  45283  suctrALT2VD  45284  eqsbc2VD  45288  simplbi2VD  45294  exbirVD  45301  exbiriVD  45302  imbi12VD  45321  sbcim2gVD  45323  simplbi2comtVD  45336  con5VD  45348  2uasbanhVD  45359  nimnbi2  45616  absnsb  47491  thincciso  49944