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  506  pm4.72  964  bianir  1074  albi  1848  spsbbi  2107  cbv2w  2369  cbv2  2435  cbv2h  2438  equvel  2488  dfeumo  2564  eu6  2602  2eu6  2684  ralbi  3120  rexbi  3121  ceqsal1t  3487  elabgtOLD  3632  euind  3687  reu6  3689  reuind  3716  replem  5249  sepex  5263  axprALT  5393  axprOLD  5403  iota4  6517  fv3  6899  elirrvOLD  9556  axprALT2  35512  r1omhfb  35517  fineqvpow  35536  r1omhfbregs  35558  nn0prpwlem  36861  nn0prpw  36862  bj-animbi  37179  bj-bi3ant  37210  bj-cbv2hv  37460  bj-ceqsalt0  37547  bj-ceqsalt1  37548  bj-bm1.3ii  37728  bj-axreprepsep  37740  dfgcd3  37996  tsbi3  38812  mapdrvallem2  42447  eu6w  43436  axc11next  45144  pm13.192  45148  exbir  45216  con5  45259  sbcim2g  45275  trsspwALT  45554  trsspwALT2  45555  sspwtr  45557  sspwtrALT  45558  pwtrVD  45560  pwtrrVD  45561  snssiALTVD  45563  sstrALT2VD  45570  sstrALT2  45571  suctrALT2VD  45572  eqsbc2VD  45576  simplbi2VD  45582  exbirVD  45589  exbiriVD  45590  imbi12VD  45609  sbcim2gVD  45611  simplbi2comtVD  45624  con5VD  45636  2uasbanhVD  45647  nimnbi2  45910  absnsb  47792  thincciso  50259