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 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  bicom1  224  pm5.74  273  bija  383  simplbi2comt  506  pm4.72  964  bianir  1072  albi  1845  spsbbi  2113  cbv2w  2375  cbv2  2441  cbv2h  2444  equvel  2494  dfeumo  2570  eu6  2608  2eu6  2690  ralbi  3126  rexbi  3127  ceqsal1t  3495  elabgtOLD  3641  euind  3696  reu6  3698  reuind  3725  replem  5253  sepex  5265  axprALT  5394  axprOLD  5404  iota4  6518  fv3  6900  elirrvOLD  9560  axprALT2  35446  r1omhfb  35449  fineqvpow  35461  r1omhfbregs  35483  nn0prpwlem  36756  nn0prpw  36757  bj-animbi  37074  bj-bi3ant  37105  bj-cbv2hv  37355  bj-ceqsalt0  37442  bj-ceqsalt1  37443  bj-bm1.3ii  37622  bj-axreprepsep  37634  dfgcd3  37890  tsbi3  38708  mapdrvallem2  42343  eu6w  43334  axc11next  45042  pm13.192  45046  exbir  45114  con5  45157  sbcim2g  45173  trsspwALT  45452  trsspwALT2  45453  sspwtr  45455  sspwtrALT  45456  pwtrVD  45458  pwtrrVD  45459  snssiALTVD  45461  sstrALT2VD  45468  sstrALT2  45469  suctrALT2VD  45470  eqsbc2VD  45474  simplbi2VD  45480  exbirVD  45487  exbiriVD  45488  imbi12VD  45507  sbcim2gVD  45509  simplbi2comtVD  45522  con5VD  45534  2uasbanhVD  45545  nimnbi2  45808  absnsb  47687  thincciso  50150