Theorem biimpr 220

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

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

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 207

This theorem is referenced by:  bicom1  221  pm5.74  270  bija  380  simplbi2comt  501  pm4.72  951  bianir  1058  albi  1818  spsbbi  2074  cbv2w  2335  cbv2  2401  cbv2h  2404  equvel  2454  dfeumo  2530  eu6  2567  2eu6  2650  ralbi  3085  rexbi  3086  ceqsal1t  3477  elabgtOLD  3636  elabgtOLDOLD  3637  euind  3692  reu6  3694  reuind  3721  sbciegftOLD  3788  sepex  5250  axprALT  5372  axprOLD  5381  iota4  6480  fv3  6858  fineqvpow  35079  nn0prpwlem  36303  nn0prpw  36304  bj-animbi  36540  bj-bi3ant  36570  bj-cbv2hv  36778  bj-ceqsalt0  36865  bj-ceqsalt1  36866  bj-bm1.3ii  37045  dfgcd3  37305  tsbi3  38122  mapdrvallem2  41632  eu6w  42657  axc11next  44388  pm13.192  44392  exbir  44462  con5  44505  sbcim2g  44521  trsspwALT  44800  trsspwALT2  44801  sspwtr  44803  sspwtrALT  44804  pwtrVD  44806  pwtrrVD  44807  snssiALTVD  44809  sstrALT2VD  44816  sstrALT2  44817  suctrALT2VD  44818  eqsbc2VD  44822  simplbi2VD  44828  exbirVD  44835  exbiriVD  44836  imbi12VD  44855  sbcim2gVD  44857  simplbi2comtVD  44870  con5VD  44882  2uasbanhVD  44893  nimnbi2  45151  absnsb  47021  thincciso  49435