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  952  bianir  1059  albi  1818  spsbbi  2073  cbv2w  2339  cbv2  2408  cbv2h  2411  equvel  2461  dfeumo  2537  eu6  2574  2eu6  2657  ralbi  3103  rexbi  3104  ceqsal1t  3514  elabgt  3672  elabgtOLD  3673  euind  3730  reu6  3732  reuind  3759  sbciegftOLD  3826  sepex  5300  axprALT  5422  axprOLD  5431  iota4  6542  fv3  6924  fineqvpow  35110  nn0prpwlem  36323  nn0prpw  36324  bj-animbi  36560  bj-bi3ant  36590  bj-cbv2hv  36798  bj-ceqsalt0  36885  bj-ceqsalt1  36886  bj-bm1.3ii  37065  dfgcd3  37325  tsbi3  38142  mapdrvallem2  41647  eu6w  42686  axc11next  44425  pm13.192  44429  exbir  44499  con5  44542  sbcim2g  44558  trsspwALT  44838  trsspwALT2  44839  sspwtr  44841  sspwtrALT  44842  pwtrVD  44844  pwtrrVD  44845  snssiALTVD  44847  sstrALT2VD  44854  sstrALT2  44855  suctrALT2VD  44856  eqsbc2VD  44860  simplbi2VD  44866  exbirVD  44873  exbiriVD  44874  imbi12VD  44893  sbcim2gVD  44895  simplbi2comtVD  44908  con5VD  44920  2uasbanhVD  44931  nimnbi2  45169  absnsb  47039  thincciso  49102