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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bicom1  224  pm5.74  273  bija  383  simplbi2comt  507  pm4.72  964  bianir  1074  albi  1851  spsbbi  2110  cbv2w  2367  cbv2  2433  cbv2h  2436  equvel  2486  dfeumo  2562  eu6  2600  2eu6  2682  ralbi  3118  rexbi  3119  ceqsal1t  3483  elabgtOLD  3627  euind  3682  reu6  3684  reuind  3711  replem  5241  sepex  5255  axprALT  5384  iota4  6520  fv3  6904  elirrvOLD  9593  axprALT2  35735  r1omhfb  35739  fineqvpow  35784  r1omhfbregs  35806  nn0prpwlem  37111  nn0prpw  37112  bj-animbi  37429  bj-bi3ant  37460  bj-cbv2hv  37710  bj-ceqsalt0  37797  bj-ceqsalt1  37798  bj-bm1.3ii  37980  bj-axreprepsep  37992  dfgcd3  38247  tsbi3  39069  mapdrvallem2  42704  eu6w  43689  axc11next  45391  pm13.192  45395  exbir  45463  con5  45506  sbcim2g  45522  trsspwALT  45801  trsspwALT2  45802  sspwtr  45804  sspwtrALT  45805  pwtrVD  45807  pwtrrVD  45808  snssiALTVD  45810  sstrALT2VD  45817  sstrALT2  45818  suctrALT2VD  45819  eqsbc2VD  45823  simplbi2VD  45829  exbirVD  45836  exbiriVD  45837  imbi12VD  45856  sbcim2gVD  45858  simplbi2comtVD  45871  con5VD  45883  2uasbanhVD  45894  nimnbi2  46180  absnsb  48098  thincciso  50562