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  950  bianir  1059  albi  1816  spsbbi  2073  cbv2w  2343  cbv2  2411  cbv2h  2414  equvel  2464  dfeumo  2540  eu6  2577  2eu6  2660  ralbi  3109  rexbi  3110  ceqsal1t  3522  elabgt  3685  elabgtOLD  3686  euind  3746  reu6  3748  reuind  3775  sbciegftOLD  3843  axprALT  5440  axpr  5446  iota4  6554  fv3  6938  fineqvpow  35072  nn0prpwlem  36288  nn0prpw  36289  bj-animbi  36525  bj-bi3ant  36555  bj-cbv2hv  36763  bj-ceqsalt0  36850  bj-ceqsalt1  36851  bj-bm1.3ii  37030  dfgcd3  37290  tsbi3  38095  mapdrvallem2  41602  eu6w  42631  axc11next  44375  pm13.192  44379  exbir  44449  con5  44493  sbcim2g  44509  trsspwALT  44789  trsspwALT2  44790  sspwtr  44792  sspwtrALT  44793  pwtrVD  44795  pwtrrVD  44796  snssiALTVD  44798  sstrALT2VD  44805  sstrALT2  44806  suctrALT2VD  44807  eqsbc2VD  44811  simplbi2VD  44817  exbirVD  44824  exbiriVD  44825  imbi12VD  44844  sbcim2gVD  44846  simplbi2comtVD  44859  con5VD  44871  2uasbanhVD  44882  nimnbi2  45070  absnsb  46942  thincciso  48716