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  2371  cbv2  2437  cbv2h  2440  equvel  2490  dfeumo  2566  eu6  2604  2eu6  2686  ralbi  3122  rexbi  3123  ceqsal1t  3489  elabgtOLD  3634  euind  3689  reu6  3691  reuind  3718  replem  5251  sepex  5265  axprALT  5395  axprOLD  5405  iota4  6522  fv3  6904  elirrvOLD  9568  axprALT2  35566  r1omhfb  35571  fineqvpow  35590  r1omhfbregs  35612  nn0prpwlem  36895  nn0prpw  36896  bj-animbi  37213  bj-bi3ant  37244  bj-cbv2hv  37494  bj-ceqsalt0  37581  bj-ceqsalt1  37582  bj-bm1.3ii  37762  bj-axreprepsep  37774  dfgcd3  38030  tsbi3  38847  mapdrvallem2  42482  eu6w  43486  axc11next  45194  pm13.192  45198  exbir  45266  con5  45309  sbcim2g  45325  trsspwALT  45604  trsspwALT2  45605  sspwtr  45607  sspwtrALT  45608  pwtrVD  45610  pwtrrVD  45611  snssiALTVD  45613  sstrALT2VD  45620  sstrALT2  45621  suctrALT2VD  45622  eqsbc2VD  45626  simplbi2VD  45632  exbirVD  45639  exbiriVD  45640  imbi12VD  45659  sbcim2gVD  45661  simplbi2comtVD  45674  con5VD  45686  2uasbanhVD  45697  nimnbi2  45960  absnsb  47842  thincciso  50308