Theorem biimpr 222

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

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

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 209

This theorem is referenced by:  bicom1  223  pm5.74  272  bija  382  simplbi2comt  503  pm4.72  958  bianir  1065  albi  1826  spsbbi  2085  cbv2w  2347  cbv2  2413  cbv2h  2416  equvel  2466  dfeumo  2542  eu6  2580  2eu6  2662  ralbi  3096  rexbi  3097  ceqsal1t  3465  elabgtOLD  3613  euind  3667  reu6  3669  reuind  3696  replem  5213  sepex  5225  axprALT  5354  axprOLD  5364  iota4  6470  fv3  6849  elirrvOLD  9507  axprALT2  35305  r1omhfb  35308  fineqvpow  35311  r1omhfbregs  35333  nn0prpwlem  36565  nn0prpw  36566  bj-animbi  36884  bj-bi3ant  36915  bj-cbv2hv  37165  bj-ceqsalt0  37252  bj-ceqsalt1  37253  bj-bm1.3ii  37432  bj-axreprepsep  37443  dfgcd3  37699  tsbi3  38517  mapdrvallem2  42152  eu6w  43141  axc11next  44865  pm13.192  44869  exbir  44938  con5  44981  sbcim2g  44997  trsspwALT  45276  trsspwALT2  45277  sspwtr  45279  sspwtrALT  45280  pwtrVD  45282  pwtrrVD  45283  snssiALTVD  45285  sstrALT2VD  45292  sstrALT2  45293  suctrALT2VD  45294  eqsbc2VD  45298  simplbi2VD  45304  exbirVD  45311  exbiriVD  45312  imbi12VD  45331  sbcim2gVD  45333  simplbi2comtVD  45346  con5VD  45358  2uasbanhVD  45369  nimnbi2  45625  absnsb  47504  thincciso  49957