Theorem biimpr 219

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

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

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 206

This theorem is referenced by:  bicom1  220  pm5.74  270  bija  380  simplbi2comt  501  pm4.72  946  bianir  1055  albi  1812  spsbbi  2068  cbv2w  2325  cbv2  2394  cbv2h  2397  equvel  2447  dfeumo  2523  eu6  2560  2eu6  2644  ralbi  3095  rexbi  3096  ceqsal1t  3497  elabgt  3654  euind  3712  reu6  3714  reuind  3741  sbciegft  3807  axprALT  5410  axpr  5416  iota4  6514  fv3  6899  fineqvpow  34585  nn0prpwlem  35697  nn0prpw  35698  bj-animbi  35925  bj-bi3ant  35957  bj-cbv2hv  36165  bj-ceqsalt0  36254  bj-ceqsalt1  36255  bj-bm1.3ii  36435  dfgcd3  36695  tsbi3  37493  mapdrvallem2  41006  axc11next  43654  pm13.192  43658  exbir  43728  con5  43772  sbcim2g  43788  trsspwALT  44068  trsspwALT2  44069  sspwtr  44071  sspwtrALT  44072  pwtrVD  44074  pwtrrVD  44075  snssiALTVD  44077  sstrALT2VD  44084  sstrALT2  44085  suctrALT2VD  44086  eqsbc2VD  44090  simplbi2VD  44096  exbirVD  44103  exbiriVD  44104  imbi12VD  44123  sbcim2gVD  44125  simplbi2comtVD  44138  con5VD  44150  2uasbanhVD  44161  nimnbi2  44347  absnsb  46222  thincciso  47857