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  381  simplbi2comt  501  pm4.72  946  bianir  1055  albi  1822  spsbbi  2077  cbv2w  2336  cbv2  2403  cbv2h  2406  equvel  2456  dfeumo  2537  eu6  2574  2eu6  2658  ralbi  3092  rexbi  3169  ceqsalt  3452  vtoclgft  3482  elabgt  3596  euind  3654  reu6  3656  reuind  3683  sbciegft  3749  axprALT  5340  axpr  5346  iota4  6399  fv3  6774  fineqvpow  32965  nn0prpwlem  34438  nn0prpw  34439  bj-animbi  34666  bj-bi3ant  34698  bj-cbv2hv  34906  bj-ceqsalt0  34996  bj-ceqsalt1  34997  bj-bm1.3ii  35162  dfgcd3  35422  tsbi3  36220  mapdrvallem2  39586  axc11next  41913  pm13.192  41917  exbir  41987  con5  42031  sbcim2g  42047  trsspwALT  42327  trsspwALT2  42328  sspwtr  42330  sspwtrALT  42331  pwtrVD  42333  pwtrrVD  42334  snssiALTVD  42336  sstrALT2VD  42343  sstrALT2  42344  suctrALT2VD  42345  eqsbc2VD  42349  simplbi2VD  42355  exbirVD  42362  exbiriVD  42363  imbi12VD  42382  sbcim2gVD  42384  simplbi2comtVD  42397  con5VD  42409  2uasbanhVD  42420  absnsb  44408  thincciso  46218