Theorem biimpr 212

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 205	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
2		simprim 164	. 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜓 → 𝜑))
3	1, 2	sylbi 209	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

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

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 199

This theorem is referenced by:  bicom1  213  pm5.74  262  bija  372  simplbi2comt  497  pm4.72  935  bianir  1042  albi  1862  cbv2h  2365  equvel  2421  euexOLD  2628  2eu6  2686  ceqsalt  3429  euind  3604  reu6  3606  reuind  3627  sbciegft  3682  axpr  5137  iota4  6117  fv3  6464  nn0prpwlem  32905  nn0prpw  32906  bj-bi3ant  33153  bj-ssbbi  33213  bj-cbv2hv  33318  bj-ceqsalt0  33443  bj-ceqsalt1  33444  bj-bm1.3ii  33596  dfgcd3  33766  tsbi3  34559  mapdrvallem2  37794  axc11next  39555  pm13.192  39559  exbir  39631  con5  39675  sbcim2g  39691  trsspwALT  39980  trsspwALT2  39981  sspwtr  39983  sspwtrALT  39984  pwtrVD  39986  pwtrrVD  39987  snssiALTVD  39989  sstrALT2VD  39996  sstrALT2  39997  suctrALT2VD  39998  eqsbc3rVD  40002  simplbi2VD  40008  exbirVD  40015  exbiriVD  40016  imbi12VD  40035  sbcim2gVD  40037  simplbi2comtVD  40050  con5VD  40062  2uasbanhVD  40073  absnsb  42089