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  270  bija  382  simplbi2comt  503  pm4.72  949  bianir  1058  albi  1821  spsbbi  2077  cbv2w  2334  cbv2  2403  cbv2h  2406  equvel  2456  dfeumo  2532  eu6  2569  2eu6  2653  ralbi  3104  rexbi  3105  ceqsal1t  3505  elabgt  3663  euind  3721  reu6  3723  reuind  3750  sbciegft  3816  axprALT  5421  axpr  5427  iota4  6525  fv3  6910  fineqvpow  34096  nn0prpwlem  35207  nn0prpw  35208  bj-animbi  35435  bj-bi3ant  35467  bj-cbv2hv  35675  bj-ceqsalt0  35764  bj-ceqsalt1  35765  bj-bm1.3ii  35945  dfgcd3  36205  tsbi3  37003  mapdrvallem2  40516  axc11next  43165  pm13.192  43169  exbir  43239  con5  43283  sbcim2g  43299  trsspwALT  43579  trsspwALT2  43580  sspwtr  43582  sspwtrALT  43583  pwtrVD  43585  pwtrrVD  43586  snssiALTVD  43588  sstrALT2VD  43595  sstrALT2  43596  suctrALT2VD  43597  eqsbc2VD  43601  simplbi2VD  43607  exbirVD  43614  exbiriVD  43615  imbi12VD  43634  sbcim2gVD  43636  simplbi2comtVD  43649  con5VD  43661  2uasbanhVD  43672  nimnbi2  43859  absnsb  45737  thincciso  47669