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  2112  cbv2w  2370  cbv2  2435  cbv2h  2438  equvel  2488  dfeumo  2564  eu6  2602  2eu6  2684  ralbi  3121  rexbi  3122  ceqsal1t  3486  elabgtOLD  3630  euind  3685  reu6  3687  reuind  3714  replem  5244  sepex  5258  axprALT  5388  iota4  6535  fv3  6923  elirrvOLD  9616  reu6f  35776  axprALT2  35815  r1omhfb  35819  fineqvpow  35882  r1omhfbregs  35904  nn0prpwlem  37287  nn0prpw  37288  bj-animbi  37605  bj-bi3ant  37636  bj-cbv2hv  37886  bj-ceqsalt0  37973  bj-ceqsalt1  37974  bj-bm1.3ii  38169  bj-axreprepsep  38181  dfgcd3  38436  tsbi3  39258  mapdrvallem2  42893  eu6w  43878  axc11next  45580  pm13.192  45584  exbir  45651  con5  45694  sbcim2g  45710  trsspwALT  45989  trsspwALT2  45990  sspwtr  45992  sspwtrALT  45993  pwtrVD  45995  pwtrrVD  45996  snssiALTVD  45998  sstrALT2VD  46005  sstrALT2  46006  suctrALT2VD  46007  eqsbc2VD  46011  simplbi2VD  46017  exbirVD  46024  exbiriVD  46025  imbi12VD  46044  sbcim2gVD  46046  simplbi2comtVD  46059  con5VD  46071  2uasbanhVD  46082  nimnbi2  46382  absnsb  48300  thincciso  50791