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  2402  cbv2h  2405  equvel  2455  dfeumo  2531  eu6  2568  2eu6  2651  ralbi  3086  rexbi  3087  ceqsal1t  3483  elabgtOLD  3642  elabgtOLDOLD  3643  euind  3698  reu6  3700  reuind  3727  sbciegftOLD  3794  sepex  5258  axprALT  5380  axprOLD  5389  iota4  6495  fv3  6879  fineqvpow  35093  nn0prpwlem  36317  nn0prpw  36318  bj-animbi  36554  bj-bi3ant  36584  bj-cbv2hv  36792  bj-ceqsalt0  36879  bj-ceqsalt1  36880  bj-bm1.3ii  37059  dfgcd3  37319  tsbi3  38136  mapdrvallem2  41646  eu6w  42671  axc11next  44402  pm13.192  44406  exbir  44476  con5  44519  sbcim2g  44535  trsspwALT  44814  trsspwALT2  44815  sspwtr  44817  sspwtrALT  44818  pwtrVD  44820  pwtrrVD  44821  snssiALTVD  44823  sstrALT2VD  44830  sstrALT2  44831  suctrALT2VD  44832  eqsbc2VD  44836  simplbi2VD  44842  exbirVD  44849  exbiriVD  44850  imbi12VD  44869  sbcim2gVD  44871  simplbi2comtVD  44884  con5VD  44896  2uasbanhVD  44907  nimnbi2  45165  absnsb  47032  thincciso  49446