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  370  simplbi2comt  655  pm4.72  919  bianir  1008  albi  1743  cbv2h  2268  equvel  2346  euex  2493  2eu6  2557  ceqsalt  3218  euind  3380  reu6  3382  reuind  3398  sbciegft  3453  axpr  4876  iota4  5838  fv3  6173  nn0prpwlem  32012  nn0prpw  32013  bj-bi3ant  32269  bj-ssbbi  32317  bj-cbv2hv  32426  bj-ceqsalt0  32573  bj-ceqsalt1  32574  tsbi3  33613  mapdrvallem2  36453  axc11next  38128  pm13.192  38132  exbir  38205  con5  38249  sbcim2g  38269  trsspwALT  38567  trsspwALT2  38568  sspwtr  38570  sspwtrALT  38571  pwtrVD  38581  pwtrrVD  38582  snssiALTVD  38584  sstrALT2VD  38591  sstrALT2  38592  suctrALT2VD  38593  eqsbc3rVD  38597  simplbi2VD  38603  exbirVD  38610  exbiriVD  38611  imbi12VD  38631  sbcim2gVD  38633  simplbi2comtVD  38646  con5VD  38658  2uasbanhVD  38669