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  1818  spsbbi  2074  cbv2w  2335  cbv2  2401  cbv2h  2404  equvel  2454  dfeumo  2530  eu6  2567  2eu6  2650  ralbi  3084  rexbi  3085  ceqsal1t  3469  elabgtOLD  3628  elabgtOLDOLD  3629  euind  3684  reu6  3686  reuind  3713  sbciegftOLD  3780  sepex  5239  axprALT  5361  axprOLD  5370  iota4  6463  fv3  6840  elirrv  9489  fineqvpow  35077  nn0prpwlem  36306  nn0prpw  36307  bj-animbi  36543  bj-bi3ant  36573  bj-cbv2hv  36781  bj-ceqsalt0  36868  bj-ceqsalt1  36869  bj-bm1.3ii  37048  dfgcd3  37308  tsbi3  38125  mapdrvallem2  41634  eu6w  42659  axc11next  44389  pm13.192  44393  exbir  44463  con5  44506  sbcim2g  44522  trsspwALT  44801  trsspwALT2  44802  sspwtr  44804  sspwtrALT  44805  pwtrVD  44807  pwtrrVD  44808  snssiALTVD  44810  sstrALT2VD  44817  sstrALT2  44818  suctrALT2VD  44819  eqsbc2VD  44823  simplbi2VD  44829  exbirVD  44836  exbiriVD  44837  imbi12VD  44856  sbcim2gVD  44858  simplbi2comtVD  44871  con5VD  44883  2uasbanhVD  44894  nimnbi2  45152  absnsb  47021  thincciso  49448