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  1850  spsbbi  2109  cbv2w  2366  cbv2  2432  cbv2h  2435  equvel  2485  dfeumo  2561  eu6  2599  2eu6  2681  ralbi  3117  rexbi  3118  ceqsal1t  3482  elabgtOLD  3626  euind  3681  reu6  3683  reuind  3710  replem  5240  sepex  5254  axprALT  5383  iota4  6519  fv3  6903  elirrvOLD  9592  axprALT2  35734  r1omhfb  35738  fineqvpow  35783  r1omhfbregs  35805  nn0prpwlem  37110  nn0prpw  37111  bj-animbi  37428  bj-bi3ant  37459  bj-cbv2hv  37709  bj-ceqsalt0  37796  bj-ceqsalt1  37797  bj-bm1.3ii  37979  bj-axreprepsep  37991  dfgcd3  38246  tsbi3  39068  mapdrvallem2  42703  eu6w  43688  axc11next  45390  pm13.192  45394  exbir  45462  con5  45505  sbcim2g  45521  trsspwALT  45800  trsspwALT2  45801  sspwtr  45803  sspwtrALT  45804  pwtrVD  45806  pwtrrVD  45807  snssiALTVD  45809  sstrALT2VD  45816  sstrALT2  45817  suctrALT2VD  45818  eqsbc2VD  45822  simplbi2VD  45828  exbirVD  45835  exbiriVD  45836  imbi12VD  45855  sbcim2gVD  45857  simplbi2comtVD  45870  con5VD  45882  2uasbanhVD  45893  nimnbi2  46179  absnsb  48097  thincciso  50561