Theorem biimpr 223

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 216	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
2		simprim 167	. 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜓 → 𝜑))
3	1, 2	sylbi 220	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bicom1  224  pm5.74  273  bija  383  simplbi2comt  507  pm4.72  964  bianir  1074  albi  1851  spsbbi  2110  cbv2w  2366  cbv2  2432  cbv2h  2435  equvel  2485  dfeumo  2561  eu6  2599  2eu6  2681  ralbi  3117  rexbi  3118  ceqsal1t  3482  elabgtOLD  3627  euind  3682  reu6  3684  reuind  3711  replem  5243  sepex  5257  axprALT  5387  axprOLD  5397  iota4  6516  fv3  6899  elirrvOLD  9577  axprALT2  35650  r1omhfb  35655  fineqvpow  35684  r1omhfbregs  35706  nn0prpwlem  37008  nn0prpw  37009  bj-animbi  37326  bj-bi3ant  37357  bj-cbv2hv  37607  bj-ceqsalt0  37694  bj-ceqsalt1  37695  bj-bm1.3ii  37875  bj-axreprepsep  37887  dfgcd3  38141  tsbi3  38948  mapdrvallem2  42583  eu6w  43587  axc11next  45295  pm13.192  45299  exbir  45367  con5  45410  sbcim2g  45426  trsspwALT  45705  trsspwALT2  45706  sspwtr  45708  sspwtrALT  45709  pwtrVD  45711  pwtrrVD  45712  snssiALTVD  45714  sstrALT2VD  45721  sstrALT2  45722  suctrALT2VD  45723  eqsbc2VD  45727  simplbi2VD  45733  exbirVD  45740  exbiriVD  45741  imbi12VD  45760  sbcim2gVD  45762  simplbi2comtVD  45775  con5VD  45787  2uasbanhVD  45798  nimnbi2  46061  absnsb  47980  thincciso  50444