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  3085  rexbi  3086  ceqsal1t  3480  elabgtOLD  3639  elabgtOLDOLD  3640  euind  3695  reu6  3697  reuind  3724  sbciegftOLD  3791  sepex  5255  axprALT  5377  axprOLD  5386  iota4  6492  fv3  6876  fineqvpow  35086  nn0prpwlem  36310  nn0prpw  36311  bj-animbi  36547  bj-bi3ant  36577  bj-cbv2hv  36785  bj-ceqsalt0  36872  bj-ceqsalt1  36873  bj-bm1.3ii  37052  dfgcd3  37312  tsbi3  38129  mapdrvallem2  41639  eu6w  42664  axc11next  44395  pm13.192  44399  exbir  44469  con5  44512  sbcim2g  44528  trsspwALT  44807  trsspwALT2  44808  sspwtr  44810  sspwtrALT  44811  pwtrVD  44813  pwtrrVD  44814  snssiALTVD  44816  sstrALT2VD  44823  sstrALT2  44824  suctrALT2VD  44825  eqsbc2VD  44829  simplbi2VD  44835  exbirVD  44842  exbiriVD  44843  imbi12VD  44862  sbcim2gVD  44864  simplbi2comtVD  44877  con5VD  44889  2uasbanhVD  44900  nimnbi2  45158  absnsb  47025  thincciso  49439