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  1814  spsbbi  2070  cbv2w  2337  cbv2  2405  cbv2h  2408  equvel  2458  dfeumo  2534  eu6  2571  2eu6  2654  ralbi  3100  rexbi  3101  ceqsal1t  3511  elabgt  3671  elabgtOLD  3672  euind  3732  reu6  3734  reuind  3761  sbciegftOLD  3829  sepex  5305  axprALT  5427  axprOLD  5436  iota4  6543  fv3  6924  fineqvpow  35088  nn0prpwlem  36304  nn0prpw  36305  bj-animbi  36541  bj-bi3ant  36571  bj-cbv2hv  36779  bj-ceqsalt0  36866  bj-ceqsalt1  36867  bj-bm1.3ii  37046  dfgcd3  37306  tsbi3  38121  mapdrvallem2  41627  eu6w  42662  axc11next  44401  pm13.192  44405  exbir  44475  con5  44519  sbcim2g  44535  trsspwALT  44815  trsspwALT2  44816  sspwtr  44818  sspwtrALT  44819  pwtrVD  44821  pwtrrVD  44822  snssiALTVD  44824  sstrALT2VD  44831  sstrALT2  44832  suctrALT2VD  44833  eqsbc2VD  44837  simplbi2VD  44843  exbirVD  44850  exbiriVD  44851  imbi12VD  44870  sbcim2gVD  44872  simplbi2comtVD  44885  con5VD  44897  2uasbanhVD  44908  nimnbi2  45106  absnsb  46976  thincciso  48848