Theorem biimpr 210

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 203	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
2		simprim 162	. 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜓 → 𝜑))
3	1, 2	sylbi 207	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

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

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 197

This theorem is referenced by:  bicom1  211  pm5.74  259  bija  369  simplbi2comt  657  pm4.72  956  bianir  1047  albi  1895  cbv2h  2414  equvel  2484  euex  2631  2eu6  2696  ceqsalt  3368  euind  3534  reu6  3536  reuind  3552  sbciegft  3607  axpr  5054  iota4  6030  fv3  6367  nn0prpwlem  32623  nn0prpw  32624  bj-bi3ant  32880  bj-ssbbi  32928  bj-cbv2hv  33037  bj-ceqsalt0  33179  bj-ceqsalt1  33180  dfgcd3  33481  tsbi3  34255  mapdrvallem2  37436  axc11next  39109  pm13.192  39113  exbir  39186  con5  39230  sbcim2g  39250  trsspwALT  39547  trsspwALT2  39548  sspwtr  39550  sspwtrALT  39551  pwtrVD  39558  pwtrrVD  39559  snssiALTVD  39561  sstrALT2VD  39568  sstrALT2  39569  suctrALT2VD  39570  eqsbc3rVD  39574  simplbi2VD  39580  exbirVD  39587  exbiriVD  39588  imbi12VD  39608  sbcim2gVD  39610  simplbi2comtVD  39623  con5VD  39635  2uasbanhVD  39646