Theorem biimpr 223

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

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

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 210

This theorem is referenced by:  bicom1  224  pm5.74  273  bija  385  simplbi2comt  505  pm4.72  947  bianir  1054  albi  1820  spsbbi  2078  cbv2w  2346  cbv2  2412  cbv2h  2415  equvel  2468  dfeumo  2595  eu6  2634  2eu6  2719  ralbi  3135  ceqsalt  3474  vtoclgft  3501  euind  3663  reu6  3665  reuind  3692  sbciegft  3756  axprALT  5288  axpr  5294  iota4  6305  fv3  6663  nn0prpwlem  33783  nn0prpw  33784  bj-animbi  34007  bj-bi3ant  34036  bj-cbv2hv  34234  bj-ceqsalt0  34324  bj-ceqsalt1  34325  bj-bm1.3ii  34481  dfgcd3  34738  tsbi3  35573  mapdrvallem2  38941  axc11next  41110  pm13.192  41114  exbir  41184  con5  41228  sbcim2g  41244  trsspwALT  41524  trsspwALT2  41525  sspwtr  41527  sspwtrALT  41528  pwtrVD  41530  pwtrrVD  41531  snssiALTVD  41533  sstrALT2VD  41540  sstrALT2  41541  suctrALT2VD  41542  eqsbc3rVD  41546  simplbi2VD  41552  exbirVD  41559  exbiriVD  41560  imbi12VD  41579  sbcim2gVD  41581  simplbi2comtVD  41594  con5VD  41606  2uasbanhVD  41617  absnsb  43619