Theorem biimpr 219

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 212	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
2		simprim 166	. 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜓 → 𝜑))
3	1, 2	sylbi 216	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

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

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 206

This theorem is referenced by:  bicom1  220  pm5.74  269  bija  382  simplbi2comt  502  pm4.72  947  bianir  1056  albi  1821  spsbbi  2077  cbv2w  2335  cbv2  2404  cbv2h  2407  equvel  2457  dfeumo  2538  eu6  2575  2eu6  2659  ralbi  3090  rexbi  3174  ceqsalt  3463  vtoclgft  3493  elabgt  3604  euind  3660  reu6  3662  reuind  3689  sbciegft  3755  axprALT  5346  axpr  5352  iota4  6418  fv3  6801  fineqvpow  33074  nn0prpwlem  34520  nn0prpw  34521  bj-animbi  34748  bj-bi3ant  34780  bj-cbv2hv  34988  bj-ceqsalt0  35078  bj-ceqsalt1  35079  bj-bm1.3ii  35244  dfgcd3  35504  tsbi3  36302  mapdrvallem2  39666  axc11next  42031  pm13.192  42035  exbir  42105  con5  42149  sbcim2g  42165  trsspwALT  42445  trsspwALT2  42446  sspwtr  42448  sspwtrALT  42449  pwtrVD  42451  pwtrrVD  42452  snssiALTVD  42454  sstrALT2VD  42461  sstrALT2  42462  suctrALT2VD  42463  eqsbc2VD  42467  simplbi2VD  42473  exbirVD  42480  exbiriVD  42481  imbi12VD  42500  sbcim2gVD  42502  simplbi2comtVD  42515  con5VD  42527  2uasbanhVD  42538  absnsb  44532  thincciso  46341